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