---

Step * of Lemma increasing_implies_le

∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  {∀[x,y:ℕk].  (f x) ≤ (f y) supposing x ≤ y} supposing increasing(f;k)
BY
{ (Unfold `guard` 0 THEN Auto) }

1
1. k : ℕ
2. f : ℕk ⟶ ℤ
3. increasing(f;k)
4. x : ℕk
5. y : ℕk
6. x ≤ y
⊢ (f x) ≤ (f y)

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index