strictMono_iff_map_neg — Mathlib

English

Let f: α → β be a map between ordered additive groups. Then f is strictly monotone iff every negative input maps to a negative output, i.e., for all a with a < 0 we have f(a) < 0.

Русский

Пусть f: α → β — отображение между упорядоченными группами. Тогда f строго монотонна тогда и только тогда, когда для всех a < 0 выполняется f(a) < 0.

LaTeX

$$$StrictMono(f) \\iff \\forall a < 0,\\; f(a) < 0$$$

Lean4

theorem strictMono_iff_map_neg : StrictMono (f : α → β) ↔ ∀ a < 0, f a < 0 :=
  strictAnti_comp_ofDual_iff.symm.trans <| strictAnti_iff_map_neg (α := αᵒᵈ) (iamhc := iamhc) _

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