antitone_iff_map_nonneg — Mathlib

English

Let α and β be ordered additive groups, and f be an order-preserving monoid homomorphism from α to β. Then f is antitone if and only if it maps nonpositive elements to nonnegative elements; equivalently, for all a ≤ 0 we have 0 ≤ f(a).

Русский

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

LaTeX

$$$Antitone(f) \\iff \\forall a \\le 0,\\; 0 \\le f(a)$$$

Lean4

theorem antitone_iff_map_nonneg : Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 ≤ f a :=
  monotone_comp_ofDual_iff.symm.trans <| monotone_iff_map_nonneg (α := αᵒᵈ) (iamhc := iamhc) _

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