---

Step * of Lemma strict-inc-lower-bound

∀[f:StrictInc]. ∀[i:ℕ].  (i ≤ (f i))
BY
{ (Auto THEN D 1 THEN (Unhide THENA Auto)) }

1
1. f : ℕ ⟶ ℕ
2. ∀j:ℕ. ∀i:ℕj.  f i < f j
3. i : ℕ
⊢ i ≤ (f i)

---

Latex:

---

Latex:
\mforall{}[f:StrictInc].  \mforall{}[i:\mBbbN{}].    (i  \mleq{}  (f  i))


By

---

Latex:
(Auto  THEN  D  1  THEN  (Unhide  THENA  Auto))

---

Home Index