strictAnti_iff_map_neg — Mathlib

English

Let f: α → β be a map between ordered additive groups. Then f is strictly anti-monotone iff ∀ a, 0 < a implies f(a) < 0.

Русский

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

LaTeX

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

Lean4

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

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