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.

source

theorem strict_mono_of_odd_strict_mono_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : strict_mono_on f (set.Ici 0)) :

strict_mono 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 strict_anti_of_odd_strict_anti_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : strict_anti_on f (set.Ici 0)) :

strict_anti 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_monotone_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : monotone_on 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_monotone_on_nonneg {G : Type u_1} {H : Type u_2} [linear_ordered_add_comm_group G] [ordered_add_comm_group H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : antitone_on 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.