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] 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} [LinearOrder α] [Preorder β] {f : α → β} {s t : Set α} {c : α} (h₁ : StrictMonoOn f s) (h₂ : StrictMonoOn f t) (hs : IsGreatest s c) (ht : IsLeast t c) : StrictMonoOn 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

theorem StrictMonoOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : α → β} (h₁ : StrictMonoOn f (Set.Iic a)) (h₂ : StrictMonoOn f (Set.Ici a)) : StrictMono f

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

theorem StrictAntiOn.union {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : α → β} {s t : Set α} {c : α} (h₁ : StrictAntiOn f s) (h₂ : StrictAntiOn f t) (hs : IsGreatest s c) (ht : IsLeast t c) : StrictAntiOn 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

theorem StrictAntiOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : α → β} (h₁ : StrictAntiOn f (Set.Iic a)) (h₂ : StrictAntiOn f (Set.Ici a)) : StrictAnti f

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

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

theorem MonotoneOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : α → β} (h₁ : MonotoneOn f (Set.Iic a)) (h₂ : MonotoneOn f (Set.Ici a)) : Monotone f

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

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

theorem AntitoneOn.Iic_union_Ici {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {f : α → β} (h₁ : AntitoneOn f (Set.Iic a)) (h₂ : AntitoneOn f (Set.Ici a)) : Antitone f

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