antitone_of_odd_of_monotoneOn_nonneg

English

If f is odd and monotone on the nonnegative part, then f is antitone on the whole group (via duality).

Русский

Если f нечётна и монотонна на неотрицательной части, то f антитонна на всей группе (через двойственность).

LaTeX

$$$\text{antitone from monotone via duality: } $$$

Lean4

/-- An odd function on a linear ordered additive commutative group is antitone on the whole group
provided that it is monotone on `Set.Ici 0`. -/
theorem antitone_of_odd_of_monotoneOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x) (h₂ : AntitoneOn f (Ici 0)) :
    Antitone f :=
  monotone_of_odd_of_monotoneOn_nonneg (H := Hᵒᵈ) h₁ h₂

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