# 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`.

source
theorem strictMono_of_odd_strictMonoOn_nonneg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictMonoOn f (Set.Ici 0)) :
StrictMono 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`.

source
theorem strictAnti_of_odd_strictAntiOn_nonneg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictAntiOn f (Set.Ici 0)) :
StrictAnti 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`.

source
theorem monotone_of_odd_of_monotoneOn_nonneg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : MonotoneOn f (Set.Ici 0)) :
Monotone 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`.

source
theorem antitone_of_odd_of_monotoneOn_nonneg {G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : AntitoneOn f (Set.Ici 0)) :
Antitone 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`.