Monotonicity on intervals #

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

In this file we prove that a function is (strictly) monotone (or antitone) on a linear order α provided that it is (strictly) monotone on (-∞, a] and on [a, +∞). This is a special case of a more general statement where one deduces monotonicity on a union from monotonicity on each set.

source

@[protected]

theorem strict_mono_on.union {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} {s t : set α} {c : α} (h₁ : strict_mono_on f s) (h₂ : strict_mono_on f t) (hs : is_greatest s c) (ht : is_least t c) :

strict_mono_on f (s ∪ t)

If f is strictly monotone both on s and t, with s to the left of t and the center point belonging to both s and t, then f is strictly monotone on s ∪ t

source

@[protected]

theorem strict_mono_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : strict_mono_on f (set.Iic a)) (h₂ : strict_mono_on f (set.Ici a)) :

strict_mono f

If f is strictly monotone both on (-∞, a] and [a, ∞), then it is strictly monotone on the whole line.

source

@[protected]

theorem strict_anti_on.union {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} {s t : set α} {c : α} (h₁ : strict_anti_on f s) (h₂ : strict_anti_on f t) (hs : is_greatest s c) (ht : is_least t c) :

strict_anti_on f (s ∪ t)

If f is strictly antitone both on s and t, with s to the left of t and the center point belonging to both s and t, then f is strictly antitone on s ∪ t

source

@[protected]

theorem strict_anti_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : strict_anti_on f (set.Iic a)) (h₂ : strict_anti_on f (set.Ici a)) :

strict_anti f

If f is strictly antitone both on (-∞, a] and [a, ∞), then it is strictly antitone on the whole line.

source

@[protected]

theorem monotone_on.union_right {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} {s t : set α} {c : α} (h₁ : monotone_on f s) (h₂ : monotone_on f t) (hs : is_greatest s c) (ht : is_least t c) :

monotone_on f (s ∪ t)

If f is monotone both on s and t, with s to the left of t and the center point belonging to both s and t, then f is monotone on s ∪ t

source

@[protected]

theorem monotone_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : monotone_on f (set.Iic a)) (h₂ : monotone_on f (set.Ici a)) :

monotone f

If f is monotone both on (-∞, a] and [a, ∞), then it is monotone on the whole line.

source

@[protected]

theorem antitone_on.union_right {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {f : α → β} {s t : set α} {c : α} (h₁ : antitone_on f s) (h₂ : antitone_on f t) (hs : is_greatest s c) (ht : is_least t c) :

antitone_on f (s ∪ t)

If f is antitone both on s and t, with s to the left of t and the center point belonging to both s and t, then f is antitone on s ∪ t

source

@[protected]

theorem antitone_on.Iic_union_Ici {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a : α} {f : α → β} (h₁ : antitone_on f (set.Iic a)) (h₂ : antitone_on f (set.Ici a)) :

antitone f

If f is antitone both on (-∞, a] and [a, ∞), then it is antitone on the whole line.