---

Step * of Lemma biject-quotient

∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.
  (Bij(A;B;f) ⇒ EquivRel(B;x,y.x R y) ⇒ Bij(x,y:A//(x R_f y);x,y:B//(x R y);quo-lift(f)))
BY
{ (Auto
   THEN (Assert EquivRel(A;x,y.x R_f y) BY
               (BLemma `preima_of_equiv_rel` THEN Auto))
   THEN (InstLemma `quo-lift_wf` [⌜A⌝;⌜B⌝;⌜f⌝;⌜R⌝]⋅ THENA Auto)
   THEN ParallelOp -4
   THEN Auto
   THEN D 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. R : B ⟶ B ⟶ ℙ
5. Inj(A;B;f)
6. Surj(A;B;f)
7. EquivRel(B;x,y.x R y)
8. EquivRel(A;x,y.x R_f y)
9. quo-lift(f) ∈ (x,y:A//(x R_f y)) ⟶ (x,y:B//(x R y))
10. a1 : x,y:A//(x R_f y)
11. a2 : x,y:A//(x R_f y)
12. (quo-lift(f) a1) = (quo-lift(f) a2) ∈ (x,y:B//(x R y))
⊢ a1 = a2 ∈ (x,y:A//(x R_f y))

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. R : B ⟶ B ⟶ ℙ
5. Inj(A;B;f)
6. Surj(A;B;f)
7. EquivRel(B;x,y.x R y)
8. EquivRel(A;x,y.x R_f y)
9. quo-lift(f) ∈ (x,y:A//(x R_f y)) ⟶ (x,y:B//(x R y))
10. Inj(x,y:A//(x R_f y);x,y:B//(x R y);quo-lift(f))
11. b : x,y:B//(x R y)
⊢ ∃a:x,y:A//(x R_f y). ((quo-lift(f) a) = b ∈ (x,y:B//(x R y)))

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.
    (Bij(A;B;f)  {}\mRightarrow{}  EquivRel(B;x,y.x  R  y)  {}\mRightarrow{}  Bij(x,y:A//(x  R\_f  y);x,y:B//(x  R  y);quo-lift(f)))


By

---

Latex:
(Auto
  THEN  (Assert  EquivRel(A;x,y.x  R\_f  y)  BY
                          (BLemma  `preima\_of\_equiv\_rel`  THEN  Auto))
  THEN  (InstLemma  `quo-lift\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelOp  -4
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index