---

Step * of Lemma increasing_is_id

∀[k:ℕ]. ∀[f:ℕk ⟶ ℕk].  ∀[i:ℕk]. ((f i) = i ∈ ℤ) supposing increasing(f;k)
BY
{ (((D 0 THENA Auto) THEN NatInd 1) THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k].    \mforall{}[i:\mBbbN{}k].  ((f  i)  =  i)  supposing  increasing(f;k)


By

---

Latex:
(((D  0  THENA  Auto)  THEN  NatInd  1)  THEN  Auto)

---

Home Index