Monotonicity on intervals #
In this file we prove that a function is (strictly) monotone (or antitone) on a linear order α
provided that it is (strictly) monotone on (-∞, a] and on [a, +∞). We also provide an order
isomorphism order_iso_Ioo_neg_one_one between the open interval (-1, 1) in a linear ordered
field and the whole field.
@[protected]
theorem
strict_mono_on.Iic_union_Ici
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : α → β}
(h₁ : strict_mono_on f (set.Iic a))
(h₂ : strict_mono_on f (set.Ici a)) :
If f is strictly monotone both on (-∞, a] and [a, ∞), then it is strictly monotone on the
whole line.
@[protected]
theorem
strict_anti_on.Iic_union_Ici
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : α → β}
(h₁ : strict_anti_on f (set.Iic a))
(h₂ : strict_anti_on f (set.Ici a)) :
If f is strictly antitone both on (-∞, a] and [a, ∞), then it is strictly antitone on the
whole line.
@[protected]
theorem
monotone_on.Iic_union_Ici
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : α → β}
(h₁ : monotone_on f (set.Iic a))
(h₂ : monotone_on f (set.Ici a)) :
monotone f
@[protected]
theorem
antitone_on.Iic_union_Ici
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[preorder β]
{a : α}
{f : α → β}
(h₁ : antitone_on f (set.Iic a))
(h₂ : antitone_on f (set.Ici a)) :
antitone f
theorem
strict_mono_of_odd_strict_mono_on_nonneg
{G : Type u_1}
{H : Type u_2}
[linear_ordered_add_comm_group G]
[ordered_add_comm_group H]
{f : G → H}
(h₁ : ∀ (x : G), f (-x) = -f x)
(h₂ : strict_mono_on f (set.Ici 0)) :
theorem
monotone_of_odd_of_monotone_on_nonneg
{G : Type u_1}
{H : Type u_2}
[linear_ordered_add_comm_group G]
[ordered_add_comm_group H]
{f : G → H}
(h₁ : ∀ (x : G), f (-x) = -f x)
(h₂ : monotone_on f (set.Ici 0)) :
monotone f
@[irreducible]
In a linear ordered field, the whole field is order isomorphic to the open interval (-1, 1).
We consider the actual implementation to be a "black box", so it is irreducible.
@[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
Union_Ioo_of_mono_of_is_glb_of_is_lub
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[linear_order β]
{f g : α → β}
{a b : β}
(hf : antitone f)
(hg : monotone g)
(ha : is_glb (set.range f) a)
(hb : is_lub (set.range g) b) :
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.Iic_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_Iic_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_Iic_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)