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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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)
:
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
strictMono_of_lt_succ
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
{ψ : α → β}
[SuccOrder α]
[IsSuccArchimedean α]
(hψ : ∀ (m : α), ψ m < ψ (Order.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
strictAnti_of_succ_lt
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
{ψ : α → β}
[SuccOrder α]
[IsSuccArchimedean α]
(hψ : ∀ (m : α), ψ (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)
:
StrictMonoOn ψ (Set.Ici n)
theorem
strictMono_of_pred_lt
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
{ψ : α → β}
[PredOrder α]
[IsPredArchimedean α]
(hψ : ∀ (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))
:
StrictAntiOn ψ (Set.Ici n)
theorem
strictAnti_of_lt_pred
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[Preorder β]
{ψ : α → β}
[PredOrder α]
[IsPredArchimedean α]
(hψ : ∀ (m : α), ψ m < ψ (Order.pred m))
:
theorem
StrictMonoOn.Iic_id_le
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
[OrderBot α]
{n : α}
{φ : α → α}
(hφ : StrictMonoOn φ (Set.Iic n))
(m : α)
:
theorem
StrictMonoOn.Ici_le_id
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[IsPredArchimedean α]
[OrderTop α]
{n : α}
{φ : α → α}
(hφ : StrictMonoOn φ (Set.Ici n))
(m : α)
: