monotone_iff_forall_lt — Mathlib

English

A function is monotone iff it preserves ≤ whenever a < b implies f(a) ≤ f(b).

Русский

Функция монотонна тогда и только тогда, когда при a < b выполняется f(a) ≤ f(b).

LaTeX

$$$$\\text{Monotone } f \\iff \\forall a

Lean4

theorem monotone_iff_forall_lt : Monotone f ↔ ∀ ⦃a b⦄, a < b → f a ≤ f b :=
  forall₂_congr fun _ _ ↦ ⟨fun hf h ↦ hf h.le, fun hf h ↦ h.eq_or_lt.elim (fun H ↦ (congr_arg _ H).le) hf⟩

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