strictMono_int_of_lt_succ — Mathlib

English

If f: ℤ → α satisfies f(n) < f(n+1) for all n, then f is strictly monotone on ℤ.

Русский

Если f: ℤ → α удовлетворяет f(n) < f(n+1) для всех n, тогда f строго монотонна на ℤ.

LaTeX

$$$\\forall f : \\mathbb{Z} \\to α, (\\forall n : \\mathbb{Z}, f n < f (n + 1)) \\Rightarrow \\mathrm{StrictMono} f$$$

Lean4

theorem strictMono_int_of_lt_succ {f : ℤ → α} (hf : ∀ n, f n < f (n + 1)) : StrictMono f :=
  Int.rel_of_forall_rel_succ_of_lt (· < ·) hf

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