---

Step * of Lemma equipollent-cardinality-le

∀[A:Type]. ∀[k:ℕ].  (A ~ ℕk ⇒ |A| ≤ k)
BY
{ (Auto THEN D -1 THEN (FLemma `biject-inverse` [-1] THEN Auto) THEN ExRepD) }

1
1. [A] : Type
2. [k] : ℕ
3. f : A ⟶ ℕk
4. Bij(A;ℕk;f)
5. g : ℕk ⟶ A
6. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
7. ∀a:A. ((g (f a)) = a ∈ A)
⊢ |A| ≤ k

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -1  THEN  (FLemma  `biject-inverse`  [-1]  THEN  Auto)  THEN  ExRepD)

---

Home Index