Documentation

Mathlib.Order.Interval.Set.Monotone

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_id_le {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : αα} (hφ : StrictMonoOn φ (Set.Iic n)) (m : α) :
m nm φ m
theorem StrictMonoOn.Ici_le_id {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : αα} (hφ : StrictMonoOn φ (Set.Ici n)) (m : α) :
n mφ m m
theorem strictMonoOn_Iic_of_lt_succ {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {ψ : αβ} [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : m < n, ψ m < ψ (Order.succ m)) :

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) :
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) :
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)) :