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} [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.

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.

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.

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.