strictAnti_of_odd_strictAntiOn_nonneg

English

If f is odd and strictly antitone on [0, ∞), then f is strictly antitone on the whole group.

Русский

Если f нечётна и строго антитонна на луче [0, ∞), то она строго антитонна на всей группе.

LaTeX

$$$\big(\forall x,\ f(-x) = -f(x)\big) \land \big(\mathrm{StrictAntiOn}(f,\, \Ici 0)\big) \Rightarrow \mathrm{StrictAnti}(f)$$$

Lean4

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

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