---

Step * of Lemma cardinality-le_functionality_wrt_equipollence

∀[A,B:Type]. ∀[k:ℕ].  (A ~ B ⇒ {|A| ≤ k ⇐⇒ |B| ≤ k})
BY
{ (Auto THEN D -1 THEN D 0 THEN Auto THEN ParallelLast THEN ExRepD) }

1
1. [A] : Type
2. [B] : Type
3. [k] : ℕ
4. f : A ⟶ B
5. Bij(A;B;f)
6. f1 : ℕk ⟶ A
7. Surj(ℕk;A;f1)
⊢ ∃f:ℕk ⟶ B. Surj(ℕk;B;f)

2
1. [A] : Type
2. [B] : Type
3. [k] : ℕ
4. f : A ⟶ B
5. Bij(A;B;f)
6. f1 : ℕk ⟶ B
7. Surj(ℕk;B;f1)
⊢ ∃f:ℕk ⟶ A. Surj(ℕk;A;f)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[k:\mBbbN{}].    (A  \msim{}  B  {}\mRightarrow{}  \{|A|  \mleq{}  k  \mLeftarrow{}{}\mRightarrow{}  |B|  \mleq{}  k\})


By

---

Latex:
(Auto  THEN  D  -1  THEN  D  0  THEN  Auto  THEN  ParallelLast  THEN  ExRepD)

---

Home Index