---

Step * of Lemma increasing_lower_bound

∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ]. ∀[x:ℕk].  ((f 0) + x) ≤ (f x) supposing increasing(f;k)
BY
{ Auto }

1
1. k : ℕ
2. f : ℕk ⟶ ℤ
3. x : ℕk
4. increasing(f;k)
⊢ ((f 0) + x) ≤ (f x)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[f:\mBbbN{}k  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[x:\mBbbN{}k].    ((f  0)  +  x)  \mleq{}  (f  x)  supposing  increasing(f;k)


By

---

Latex:
Auto

---

Home Index