monotone_iff_map_nonneg — Mathlib

English

Monotone maps correspond to nonnegativity preservation on nonnegative inputs.

Русский

Монотонные отображения эквивалентны сохранению неотрицательности на неотрицательных аргументах.

LaTeX

$$Iff (Monotone(f)) (∀ a, a ≥ 0 → f(a) ≥ 0)$$

Lean4

theorem monotone_iff_map_nonneg [iamhc : AddMonoidHomClass F α β] : Monotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a :=
  ⟨fun h a => by
    rw [← map_zero f]
    apply h, fun h a b hl => by
    rw [← sub_add_cancel b a, map_add f]
    exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)⟩

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