---

Step * of Lemma increasing_le

∀[k,m:ℕ].  k ≤ m supposing ∃f:ℕk ⟶ ℕm. increasing(f;k)
BY
{ ((((D 0 THENA Auto) THEN primNatInd 1) THEN Auto') THEN ExRepD) }

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

---

Latex:

---

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


By

---

Latex:
((((D  0  THENA  Auto)  THEN  primNatInd  1)  THEN  Auto')  THEN  ExRepD)

---

Home Index