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` THEN Auto) }

1
1. : ℕ
2. : ℕk ⟶ ℤ
3. increasing(f;k)
4. : ℕk
5. : ℕ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