# mathlib3documentation

order.monotone.odd

# Monotonicity of odd functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An odd function on a linear ordered additive commutative group G is monotone on the whole group provided that is is monotone on set.Ici 0, see monotone_of_odd_of_monotone_on_nonneg. We also prove versions of this lemma for antitone, strict_mono, and strict_anti.

theorem strict_mono_of_odd_strict_mono_on_nonneg {G : Type u_1} {H : Type u_2} {f : G H} (h₁ : (x : G), f (-x) = -f x) (h₂ : (set.Ici 0)) :

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 strict_anti_of_odd_strict_anti_on_nonneg {G : Type u_1} {H : Type u_2} {f : G H} (h₁ : (x : G), f (-x) = -f x) (h₂ : (set.Ici 0)) :

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_monotone_on_nonneg {G : Type u_1} {H : Type u_2} {f : G H} (h₁ : (x : G), f (-x) = -f x) (h₂ : (set.Ici 0)) :

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_monotone_on_nonneg {G : Type u_1} {H : Type u_2} {f : G H} (h₁ : (x : G), f (-x) = -f x) (h₂ : (set.Ici 0)) :

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.