rel_of_forall_rel_succ_of_le — Mathlib

English

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

Русский

Если f: ℤ → α удовлетворяет 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 rel_of_forall_rel_succ_of_le (r : β → β → Prop) [IsRefl β r] [IsTrans β r] {f : ℤ → β}
    (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a ≤ b) : r (f a) (f b) :=
  hab.eq_or_lt.elim (fun h ↦ h ▸ refl _) fun h' ↦ Int.rel_of_forall_rel_succ_of_lt r h h'

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