# Documentation

Mathlib.Order.Monotone.Union

# Monotonicity on intervals #

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]∞, 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.

theorem StrictMonoOn.union {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} {t : Set α} {c : α} (h₁ : ) (h₂ : ) (hs : ) (ht : IsLeast t c) :

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∪ t

theorem StrictMonoOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {a : α} {f : αβ} (h₁ : StrictMonoOn f ()) (h₂ : StrictMonoOn f ()) :

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

theorem StrictAntiOn.union {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} {t : Set α} {c : α} (h₁ : ) (h₂ : ) (hs : ) (ht : IsLeast t c) :

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∪ t

theorem StrictAntiOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {a : α} {f : αβ} (h₁ : StrictAntiOn f ()) (h₂ : StrictAntiOn f ()) :

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

theorem MonotoneOn.union_right {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} {t : Set α} {c : α} (h₁ : ) (h₂ : ) (hs : ) (ht : IsLeast t c) :
MonotoneOn 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∪ t

theorem MonotoneOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {a : α} {f : αβ} (h₁ : MonotoneOn f ()) (h₂ : MonotoneOn f ()) :

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

theorem AntitoneOn.union_right {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} {t : Set α} {c : α} (h₁ : ) (h₂ : ) (hs : ) (ht : IsLeast t c) :
AntitoneOn 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∪ t

theorem AntitoneOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {a : α} {f : αβ} (h₁ : AntitoneOn f ()) (h₂ : AntitoneOn f ()) :

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