---

Step * of Lemma equipollent-quotient

∀[A:Type]. ∀E:A ⟶ A ⟶ 𝔹. A ~ a:x,y:A//(↑E[x;y]) × {b:A| ↑E[a;b]}  supposing EquivRel(A;x,y.↑E[x;y])
BY
{ ((Auto THEN All (Unfold `so_apply`))
   THEN (Assert E ∈ (x,y:A//(↑(E x y))) ⟶ A ⟶ 𝔹 BY
               ((ExtWith [`z'] [⌜A ⟶ A ⟶ 𝔹⌝]⋅ THENA Auto THEN Auto')
                THEN D -1
                THEN Auto
                THEN Ext
                THEN Auto
                THEN BLemma `iff_imp_equal_bool`
                THEN EAuto 1))
   ) }

1
.....aux..... 
1. A : Type
2. E : A ⟶ A ⟶ 𝔹
3. EquivRel(A;x,y.↑(E x y))
4. z : Base
5. z1 : Base
6. z = z1 ∈ (x,y:A//(↑(E x y)))
7. z ∈ A
8. z1 ∈ A
9. ↑(E z z1)
10. x : A
11. ↑(E z x)
⊢ ↑(E z1 x)

2
1. [A] : Type
2. E : A ⟶ A ⟶ 𝔹
3. EquivRel(A;x,y.↑(E x y))
4. E ∈ (x,y:A//(↑(E x y))) ⟶ A ⟶ 𝔹
⊢ A ~ a:x,y:A//(↑(E x y)) × {b:A| ↑(E a b)} 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  A  \msim{}  a:x,y:A//(\muparrow{}E[x;y])  \mtimes{}  \{b:A|  \muparrow{}E[a;b]\}    supposing  EquivRel(A;x,y.\muparrow{}E[x;y]\000C)


By

---

Latex:
((Auto  THEN  All  (Unfold  `so\_apply`))
  THEN  (Assert  E  \mmember{}  (x,y:A//(\muparrow{}(E  x  y)))  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}  BY
                          ((ExtWith  [`z']  [\mkleeneopen{}A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}]\mcdot{}  THENA  Auto  THEN  Auto')
                            THEN  D  -1
                            THEN  Auto
                            THEN  Ext
                            THEN  Auto
                            THEN  BLemma  `iff\_imp\_equal\_bool`
                            THEN  EAuto  1))
  )

---

Home Index