---

Step * of Lemma one_one_corr_equipollent

∀[A,B:Type].  (1-1-Corresp(A;B) ⇐⇒ A ~ B)
BY
{ (Intros THEN RWO "equipollent-iff-inverse-funs" 0 THEN Auto THEN D -1 THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. InvFuns(A;B;f;g)
⊢ ∃p:A ⟶ B × (B ⟶ A) [InvFuns(A;B;fst(p);snd(p))]

2
1. [A] : Type
2. [B] : Type
3. p : A ⟶ B × (B ⟶ A)
4. [%2] : InvFuns(A;B;fst(p);snd(p))
⊢ 1-1-Corresp(A;B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (1-1-Corresp(A;B)  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  B)


By

---

Latex:
(Intros  THEN  RWO  "equipollent-iff-inverse-funs"  0  THEN  Auto  THEN  D  -1  THEN  ExRepD)

---

Home Index