Monotonicity on intervals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that set.Ici etc are monotone/antitone functions. We also prove some lemmas
about functions monotone on intervals in succ_orders.
@[protected]
theorem
monotone_on.Ici
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone_on f s) :
antitone_on (λ (x : α), set.Ici (f x)) s
@[protected]
theorem
antitone_on.Ici
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone_on f s) :
monotone_on (λ (x : α), set.Ici (f x)) s
@[protected]
theorem
monotone_on.Iic
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone_on f s) :
monotone_on (λ (x : α), set.Iic (f x)) s
@[protected]
theorem
antitone_on.Iic
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone_on f s) :
antitone_on (λ (x : α), set.Iic (f x)) s
@[protected]
theorem
monotone_on.Ioi
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone_on f s) :
antitone_on (λ (x : α), set.Ioi (f x)) s
@[protected]
theorem
antitone_on.Ioi
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone_on f s) :
monotone_on (λ (x : α), set.Ioi (f x)) s
@[protected]
theorem
monotone_on.Iio
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : monotone_on f s) :
monotone_on (λ (x : α), set.Iio (f x)) s
@[protected]
theorem
antitone_on.Iio
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f : α → β}
{s : set α}
(hf : antitone_on f s) :
antitone_on (λ (x : α), set.Iio (f x)) s
@[protected]
theorem
monotone_on.Icc
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : monotone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : α), set.Icc (f x) (g x)) s
@[protected]
theorem
antitone_on.Icc
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : antitone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : α), set.Icc (f x) (g x)) s
@[protected]
theorem
monotone_on.Ico
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : monotone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : α), set.Ico (f x) (g x)) s
@[protected]
theorem
antitone_on.Ico
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : antitone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : α), set.Ico (f x) (g x)) s
@[protected]
theorem
monotone_on.Ioc
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : monotone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : α), set.Ioc (f x) (g x)) s
@[protected]
theorem
antitone_on.Ioc
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : antitone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : α), set.Ioc (f x) (g x)) s
@[protected]
theorem
monotone_on.Ioo
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : monotone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : α), set.Ioo (f x) (g x)) s
@[protected]
theorem
antitone_on.Ioo
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{f g : α → β}
{s : set α}
(hf : antitone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : α), set.Ioo (f x) (g x)) s
theorem
strict_mono_on.Iic_id_le
{α : Type u_1}
[partial_order α]
[succ_order α]
[is_succ_archimedean α]
[order_bot α]
{n : α}
{φ : α → α}
(hφ : strict_mono_on φ (set.Iic n))
(m : α)
(H : m ≤ n) :
m ≤ φ m
theorem
strict_mono_on.Ici_le_id
{α : Type u_1}
[partial_order α]
[pred_order α]
[is_pred_archimedean α]
[order_top α]
{n : α}
{φ : α → α}
(hφ : strict_mono_on φ (set.Ici n))
(m : α) :
theorem
strict_mono_on_Iic_of_lt_succ
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
{ψ : α → β}
[succ_order α]
[is_succ_archimedean α]
{n : α}
(hψ : ∀ (m : α), m < n → ψ m < ψ (order.succ m)) :
strict_mono_on ψ (set.Iic n)
A function ψ on a succ_order is strictly monotone before some n if for all m such that
m < n, we have ψ m < ψ (succ m).
theorem
strict_anti_on_Iic_of_succ_lt
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
{ψ : α → β}
[succ_order α]
[is_succ_archimedean α]
{n : α}
(hψ : ∀ (m : α), m < n → ψ (order.succ m) < ψ m) :
strict_anti_on ψ (set.Iic n)
theorem
strict_mono_on_Ici_of_pred_lt
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
{ψ : α → β}
[pred_order α]
[is_pred_archimedean α]
{n : α}
(hψ : ∀ (m : α), n < m → ψ (order.pred m) < ψ m) :
strict_mono_on ψ (set.Ici n)
theorem
strict_anti_on_Ici_of_lt_pred
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[preorder β]
{ψ : α → β}
[pred_order α]
[is_pred_archimedean α]
{n : α}
(hψ : ∀ (m : α), n < m → ψ m < ψ (order.pred m)) :
strict_anti_on ψ (set.Ici n)