---

Step * of Lemma finite'_functionality_wrt_equipollent

∀[A,B:Type].  (A ~ B ⇒ (finite'(A) ⇐⇒ finite'(B)))
BY
{ (Auto THEN ParallelLast THEN RepeatFor 2 (D -2) THEN Auto THEN RenameVar `g' (-2)) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Inj(A;B;f)
5. Surj(A;B;f)
6. ∀f:A ⟶ A. (Inj(A;A;f) ⇒ Surj(A;A;f))
7. g : B ⟶ B
8. Inj(B;B;g)
⊢ Surj(B;B;g)

2
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Inj(A;B;f)
5. Surj(A;B;f)
6. ∀f:B ⟶ B. (Inj(B;B;f) ⇒ Surj(B;B;f))
7. g : A ⟶ A
8. Inj(A;A;g)
⊢ Surj(A;A;g)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (A  \msim{}  B  {}\mRightarrow{}  (finite'(A)  \mLeftarrow{}{}\mRightarrow{}  finite'(B)))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  RepeatFor  2  (D  -2)  THEN  Auto  THEN  RenameVar  `g'  (-2))

---

Home Index