monotone_nat_of_le_succ — Mathlib

English

If f: ℕ → α satisfies f(n) ≤ f(n+1) for all n, then f is monotone: for all a ≤ b, f(a) ≤ f(b).

Русский

Если f: ℕ → α удовлетворяет f(n) ≤ f(n+1) для всех n, то функция монотонна: для любых a ≤ b выполняется f(a) ≤ f(b).

LaTeX

$$$\\forall {\\alpha} [\\mathrm{Preorder } \\alpha] {f : \\mathbb{N} \\to \\alpha}, (\\forall n, f n \\le f (n + 1)) \\Rightarrow \\forall a b : \\mathbb{N}, a \\le b \\Rightarrow f a \\le f b$$$

Lean4

theorem monotone_nat_of_le_succ {f : ℕ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f :=
  Nat.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

Похожие утверждения