English
If f is odd, i.e., f(−x) = −f(x) for all x, and f is strictly monotone on the nonnegative ray [0, ∞), then f is strictly monotone on the whole group.
Русский
Если функция нечётна, то есть f(−x) = −f(x) для всех x, и она строго монотонна на луче [0, ∞), то она строго монотонна на всей группе.
LaTeX
$$$\big(\forall x,\ f(-x) = -f(x)\big) \land \big(\mathrm{StrictMonoOn}(f,\, \Ici 0)\big) \Rightarrow \mathrm{StrictMono}(f)$$$
Lean4
/-- An odd function on a linear ordered additive commutative group is strictly monotone on the whole
group provided that it is strictly monotone on `Set.Ici 0`. -/
theorem strictMono_of_odd_strictMonoOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x) (h₂ : StrictMonoOn f (Ici 0)) :
StrictMono f := by
refine StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 ?_) h₂
rw [← h₁, ← h₁]
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)
