strictAnti_iff_map_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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