monotone_of_odd_of_monotoneOn_nonneg

English

If f is odd and monotone on the nonnegative part, then f is monotone on the whole group.

Русский

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

LaTeX

$$$(\forall x, f(-x) = -f(x)) \land (\mathrm{MonotoneOn}(f,\, \Ici 0)) \Rightarrow \mathrm{Monotone}(f)$$$

Lean4

/-- An odd function on a linear ordered additive commutative group is monotone on the whole group
provided that it is monotone on `Set.Ici 0`. -/
theorem monotone_of_odd_of_monotoneOn_nonneg {f : G → H} (h₁ : ∀ x, f (-x) = -f x) (h₂ : MonotoneOn f (Ici 0)) :
    Monotone f := by
  refine MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 ?_) h₂
  rw [← h₁, ← h₁]
  exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)

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