---

Step * of Lemma cardinality-le_functionality

∀[T:Type]. ∀n:ℕ+. ∀[m:ℕ]. {|T| ≤ n ⇒ |T| ≤ m} supposing n ≤ m
BY
{ (Auto THEN (D 0 THENA Auto) THEN ParallelLast THEN ExRepD) }

1
1. [T] : Type
2. n : ℕ+
3. [m] : ℕ
4. n ≤ m
5. f : ℕn ⟶ T
6. Surj(ℕn;T;f)
⊢ ∃f:ℕm ⟶ T. Surj(ℕm;T;f)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}[m:\mBbbN{}].  \{|T|  \mleq{}  n  {}\mRightarrow{}  |T|  \mleq{}  m\}  supposing  n  \mleq{}  m


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  ParallelLast  THEN  ExRepD)

---

Home Index