---

Step * of Lemma injection_le

∀[k,m:ℕ].  k ≤ m supposing ∃f:ℕk ⟶ ℕm. Inj(ℕk;ℕm;f)
BY
{ (InductionOnNat THEN Auto THEN Assert ⌜(k - 1) ≤ (m - 1)⌝⋅ THEN Auto THEN ExRepD) }

1
1. k : ℤ
2. 0 < k
3. ∀[m:ℕ]. (k - 1) ≤ m supposing ∃f:ℕk - 1 ⟶ ℕm. Inj(ℕk - 1;ℕm;f)
4. m : ℕ
5. f : ℕk ⟶ ℕm
6. Inj(ℕk;ℕm;f)
⊢ (k - 1) ≤ (m - 1)

---

Latex:

---

Latex:
\mforall{}[k,m:\mBbbN{}].    k  \mleq{}  m  supposing  \mexists{}f:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m.  Inj(\mBbbN{}k;\mBbbN{}m;f)


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  Assert  \mkleeneopen{}(k  -  1)  \mleq{}  (m  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  ExRepD)

---

Home Index