Monotonicity on intervals

In this file we prove that Set.Ici etc. are monotone/antitone functions. We also prove some lemmas about functions monotone on intervals in SuccOrders.

theorem antitone_Ici {α : Type u_1} [Preorder α] : Antitone Set.Ici

theorem monotone_Iic {α : Type u_1} [Preorder α] : Monotone Set.Iic

theorem antitone_Ioi {α : Type u_1} [Preorder α] : Antitone Set.Ioi

theorem monotone_Iio {α : Type u_1} [Preorder α] : Monotone Set.Iio

theorem Monotone.Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Antitone fun (x : α) => Set.Ici (f x)

theorem MonotoneOn.Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : AntitoneOn (fun (x : α) => Set.Ici (f x)) s

theorem Antitone.Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Monotone fun (x : α) => Set.Ici (f x)

theorem AntitoneOn.Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : MonotoneOn (fun (x : α) => Set.Ici (f x)) s

theorem Monotone.Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Monotone fun (x : α) => Set.Iic (f x)

theorem MonotoneOn.Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : MonotoneOn (fun (x : α) => Set.Iic (f x)) s

theorem Antitone.Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Antitone fun (x : α) => Set.Iic (f x)

theorem AntitoneOn.Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : AntitoneOn (fun (x : α) => Set.Iic (f x)) s

theorem Monotone.Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Antitone fun (x : α) => Set.Ioi (f x)

theorem MonotoneOn.Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : AntitoneOn (fun (x : α) => Set.Ioi (f x)) s

theorem Antitone.Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Monotone fun (x : α) => Set.Ioi (f x)

theorem AntitoneOn.Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : MonotoneOn (fun (x : α) => Set.Ioi (f x)) s

theorem Monotone.Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Monotone fun (x : α) => Set.Iio (f x)

theorem MonotoneOn.Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : MonotoneOn f s) : MonotoneOn (fun (x : α) => Set.Iio (f x)) s

theorem Antitone.Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Antitone fun (x : α) => Set.Iio (f x)

theorem AntitoneOn.Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hf : AntitoneOn f s) : AntitoneOn (fun (x : α) => Set.Iio (f x)) s

theorem Monotone.Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) : Antitone fun (x : α) => Set.Icc (f x) (g x)

theorem MonotoneOn.Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun (x : α) => Set.Icc (f x) (g x)) s

theorem Antitone.Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun (x : α) => Set.Icc (f x) (g x)

theorem AntitoneOn.Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun (x : α) => Set.Icc (f x) (g x)) s

theorem Monotone.Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) : Antitone fun (x : α) => Set.Ico (f x) (g x)

theorem MonotoneOn.Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun (x : α) => Set.Ico (f x) (g x)) s

theorem Antitone.Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun (x : α) => Set.Ico (f x) (g x)

theorem AntitoneOn.Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun (x : α) => Set.Ico (f x) (g x)) s

theorem Monotone.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) : Antitone fun (x : α) => Set.Ioc (f x) (g x)

theorem MonotoneOn.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun (x : α) => Set.Ioc (f x) (g x)) s

theorem Antitone.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun (x : α) => Set.Ioc (f x) (g x)

theorem AntitoneOn.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun (x : α) => Set.Ioc (f x) (g x)) s

theorem Monotone.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Monotone f) (hg : Antitone g) : Antitone fun (x : α) => Set.Ioo (f x) (g x)

theorem MonotoneOn.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun (x : α) => Set.Ioo (f x) (g x)) s

theorem Antitone.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun (x : α) => Set.Ioo (f x) (g x)

theorem AntitoneOn.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun (x : α) => Set.Ioo (f x) (g x)) s

theorem iUnion_Ioo_of_mono_of_isGLB_of_isLUB {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [LinearOrder β] {f g : α → β} {a b : β} (hf : Antitone f) (hg : Monotone g) (ha : IsGLB (Set.range f) a) (hb : IsLUB (Set.range g) b) : ⋃ (x : α), Set.Ioo (f x) (g x) = Set.Ioo a b

theorem strictMonoOn_Iic_of_lt_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m < n, ψ m < ψ (Order.succ m)) : StrictMonoOn ψ (Set.Iic n)

A function ψ on a SuccOrder is strictly monotone before some n if for all m such that m < n, we have ψ m < ψ (succ m).

theorem strictAntiOn_Iic_of_succ_lt {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m < n, ψ (Order.succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n)

theorem strictMonoOn_Ici_of_pred_lt {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ (m : α), n < m → ψ (Order.pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n)

theorem strictAntiOn_Ici_of_lt_pred {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : α → β} [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ (m : α), n < m → ψ m < ψ (Order.pred m)) : StrictAntiOn ψ (Set.Ici n)

theorem StrictMonoOn.Iic_id_le {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Iic n)) (m : α) : m ≤ n → m ≤ φ m

theorem StrictMonoOn.Ici_le_id {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α} (hφ : StrictMonoOn φ (Set.Ici n)) (m : α) : n ≤ m → φ m ≤ m