# Documentation

Mathlib.Data.Set.Intervals.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} [] :
Antitone Set.Ici
theorem monotone_Iic {α : Type u_1} [] :
Monotone Set.Iic
theorem antitone_Ioi {α : Type u_1} [] :
Antitone Set.Ioi
theorem monotone_Iio {α : Type u_1} [] :
Monotone Set.Iio
theorem Monotone.Ici {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Antitone fun x => Set.Ici (f x)
theorem MonotoneOn.Ici {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
AntitoneOn (fun x => Set.Ici (f x)) s
theorem Antitone.Ici {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Monotone fun x => Set.Ici (f x)
theorem AntitoneOn.Ici {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
MonotoneOn (fun x => Set.Ici (f x)) s
theorem Monotone.Iic {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Monotone fun x => Set.Iic (f x)
theorem MonotoneOn.Iic {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
MonotoneOn (fun x => Set.Iic (f x)) s
theorem Antitone.Iic {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Antitone fun x => Set.Iic (f x)
theorem AntitoneOn.Iic {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
AntitoneOn (fun x => Set.Iic (f x)) s
theorem Monotone.Ioi {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Antitone fun x => Set.Ioi (f x)
theorem MonotoneOn.Ioi {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
AntitoneOn (fun x => Set.Ioi (f x)) s
theorem Antitone.Ioi {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Monotone fun x => Set.Ioi (f x)
theorem AntitoneOn.Ioi {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
MonotoneOn (fun x => Set.Ioi (f x)) s
theorem Monotone.Iio {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Monotone fun x => Set.Iio (f x)
theorem MonotoneOn.Iio {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
MonotoneOn (fun x => Set.Iio (f x)) s
theorem Antitone.Iio {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :
Antitone fun x => Set.Iio (f x)
theorem AntitoneOn.Iio {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ) :
AntitoneOn (fun x => Set.Iio (f x)) s
theorem Monotone.Icc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun x => Set.Icc (f x) (g x)
theorem MonotoneOn.Icc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun x => Set.Icc (f x) (g x)) s
theorem Antitone.Icc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun x => Set.Icc (f x) (g x)
theorem AntitoneOn.Icc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (fun x => Set.Icc (f x) (g x)) s
theorem Monotone.Ico {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun x => Set.Ico (f x) (g x)
theorem MonotoneOn.Ico {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun x => Set.Ico (f x) (g x)) s
theorem Antitone.Ico {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun x => Set.Ico (f x) (g x)
theorem AntitoneOn.Ico {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (fun x => Set.Ico (f x) (g x)) s
theorem Monotone.Ioc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun x => Set.Ioc (f x) (g x)
theorem MonotoneOn.Ioc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun x => Set.Ioc (f x) (g x)) s
theorem Antitone.Ioc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun x => Set.Ioc (f x) (g x)
theorem AntitoneOn.Ioc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (fun x => Set.Ioc (f x) (g x)) s
theorem Monotone.Ioo {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun x => Set.Ioo (f x) (g x)
theorem MonotoneOn.Ioo {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun x => Set.Ioo (f x) (g x)) s
theorem Antitone.Ioo {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun x => Set.Ioo (f x) (g x)
theorem AntitoneOn.Ioo {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
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} [] [] {f : αβ} {g : αβ} {a : β} {b : β} (hf : ) (hg : ) (ha : IsGLB () a) (hb : IsLUB () b) :
⋃ (x : α), Set.Ioo (f x) (g x) = Set.Ioo a b
theorem StrictMonoOn.Iic_id_le {α : Type u_1} [] [] [] {n : α} {φ : αα} (hφ : StrictMonoOn φ ()) (m : α) :
m nm φ m
theorem StrictMonoOn.Ici_le_id {α : Type u_1} [] [] [] {n : α} {φ : αα} (hφ : StrictMonoOn φ ()) (m : α) :
n mφ m m
theorem strictMonoOn_Iic_of_lt_succ {α : Type u_1} {β : Type u_2} [] [] {ψ : αβ} [] {n : α} (hψ : ∀ (m : α), m < nψ 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} [] [] {ψ : αβ} [] {n : α} (hψ : ∀ (m : α), m < nψ () < ψ m) :
theorem strictMonoOn_Ici_of_pred_lt {α : Type u_1} {β : Type u_2} [] [] {ψ : αβ} [] {n : α} (hψ : ∀ (m : α), n < mψ () < ψ m) :
theorem strictAntiOn_Ici_of_lt_pred {α : Type u_1} {β : Type u_2} [] [] {ψ : αβ} [] {n : α} (hψ : ∀ (m : α), n < mψ m < ψ ()) :