# Documentation

Mathlib.Order.Monotone.Odd

# Monotonicity of odd functions #

An odd function on a linear ordered additive commutative group G is monotone on the whole group provided that it is monotone on Set.Ici 0, see monotone_of_odd_of_monotoneOn_nonneg. We also prove versions of this lemma for Antitone, StrictMono, and StrictAnti.

theorem strictMono_of_odd_strictMonoOn_nonneg {G : Type u_1} {H : Type u_2} {f : GH} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictMonoOn f ()) :

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 strictAnti_of_odd_strictAntiOn_nonneg {G : Type u_1} {H : Type u_2} {f : GH} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictAntiOn f ()) :

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 monotone_of_odd_of_monotoneOn_nonneg {G : Type u_1} {H : Type u_2} {f : GH} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : MonotoneOn f ()) :

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 antitone_of_odd_of_monotoneOn_nonneg {G : Type u_1} {H : Type u_2} {f : GH} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : AntitoneOn f ()) :

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.