monotone_int_of_le_succ — Mathlib

English

Same as Monotone Int: if f(n) ≤ f(n+1) for all integers n, then f is monotone on ℤ.

Русский

То же самое: если f(n) ≤ f(n+1) для всех целых n, то f монотонна на ℤ.

LaTeX

$$$\\forall f : \\mathbb{Z} \\to α, (\\forall n : \\mathbb{Z}, f n \\le f (n + 1)) \\Rightarrow \\forall a b : \\mathbb{Z}, a \\le b \\Rightarrow f a \\le f b$$$

Lean4

theorem monotone_int_of_le_succ {f : ℤ → α} (hf : ∀ n, f n ≤ f (n + 1)) : Monotone f :=
  Int.rel_of_forall_rel_succ_of_le (· ≤ ·) hf

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