---

Step * of Lemma increasing_implies

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

1
1. k : ℕ
2. f : ℕk ⟶ ℤ
3. ∀i:ℕk - 1. f i < f (i + 1)
4. x : ℕk
5. y : ℕk
6. x < y
⊢ f x < f y

---

Latex:

---

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


By

---

Latex:
((Unfold  `guard`  0  THEN  Auto)  THEN  All  (Unfold  `increasing`))

---

Home Index