Order continuity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We say that a function is left order continuous if it sends all least upper bounds to least upper bounds. The order dual notion is called right order continuity.
For monotone functions ℝ → ℝ these notions correspond to the usual left and right continuity.
We prove some basic lemmas (map_sup, map_Sup etc) and prove that an rel_iso is both left
and right order continuous.
Definitions #
A function f between preorders is left order continuous if it preserves all suprema. We
define it using is_lub instead of Sup so that the proof works both for complete lattices and
conditionally complete lattices.
A function f between preorders is right order continuous if it preserves all infima. We
define it using is_glb instead of Inf so that the proof works both for complete lattices and
conditionally complete lattices.
@[protected]
theorem
left_ord_continuous.map_is_greatest
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : left_ord_continuous f)
{s : set α}
{x : α}
(h : is_greatest s x) :
is_greatest (f '' s) (f x)
theorem
left_ord_continuous.mono
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : left_ord_continuous f) :
monotone f
theorem
left_ord_continuous.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
(hg : left_ord_continuous g)
(hf : left_ord_continuous f) :
left_ord_continuous (g ∘ f)
@[protected]
theorem
left_ord_continuous.iterate
{α : Type u}
[preorder α]
{f : α → α}
(hf : left_ord_continuous f)
(n : ℕ) :
theorem
left_ord_continuous.map_sup
{α : Type u}
{β : Type v}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(hf : left_ord_continuous f)
(x y : α) :
theorem
left_ord_continuous.le_iff
{α : Type u}
{β : Type v}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(hf : left_ord_continuous f)
(h : function.injective f)
{x y : α} :
theorem
left_ord_continuous.lt_iff
{α : Type u}
{β : Type v}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(hf : left_ord_continuous f)
(h : function.injective f)
{x y : α} :
def
left_ord_continuous.to_order_embedding
{α : Type u}
{β : Type v}
[semilattice_sup α]
[semilattice_sup β]
(f : α → β)
(hf : left_ord_continuous f)
(h : function.injective f) :
α ↪o β
Convert an injective left order continuous function to an order embedding.
Equations
- left_ord_continuous.to_order_embedding f hf h = {to_embedding := {to_fun := f, inj' := h}, map_rel_iff' := _}
@[simp]
theorem
left_ord_continuous.coe_to_order_embedding
{α : Type u}
{β : Type v}
[semilattice_sup α]
[semilattice_sup β]
{f : α → β}
(hf : left_ord_continuous f)
(h : function.injective f) :
⇑(left_ord_continuous.to_order_embedding f hf h) = f
theorem
left_ord_continuous.map_Sup'
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : left_ord_continuous f)
(s : set α) :
f (has_Sup.Sup s) = has_Sup.Sup (f '' s)
theorem
left_ord_continuous.map_Sup
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : left_ord_continuous f)
(s : set α) :
f (has_Sup.Sup s) = ⨆ (x : α) (H : x ∈ s), f x
theorem
left_ord_continuous.map_supr
{α : Type u}
{β : Type v}
{ι : Sort x}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : left_ord_continuous f)
(g : ι → α) :
theorem
left_ord_continuous.map_cSup
{α : Type u}
{β : Type v}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{f : α → β}
(hf : left_ord_continuous f)
{s : set α}
(sne : s.nonempty)
(sbdd : bdd_above s) :
f (has_Sup.Sup s) = has_Sup.Sup (f '' s)
theorem
left_ord_continuous.map_csupr
{α : Type u}
{β : Type v}
{ι : Sort x}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
{f : α → β}
(hf : left_ord_continuous f)
{g : ι → α}
(hg : bdd_above (set.range g)) :
@[protected]
theorem
right_ord_continuous.mono
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : right_ord_continuous f) :
monotone f
theorem
right_ord_continuous.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β}
(hg : right_ord_continuous g)
(hf : right_ord_continuous f) :
right_ord_continuous (g ∘ f)
@[protected]
theorem
right_ord_continuous.iterate
{α : Type u}
[preorder α]
{f : α → α}
(hf : right_ord_continuous f)
(n : ℕ) :
theorem
right_ord_continuous.map_inf
{α : Type u}
{β : Type v}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(hf : right_ord_continuous f)
(x y : α) :
theorem
right_ord_continuous.le_iff
{α : Type u}
{β : Type v}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(hf : right_ord_continuous f)
(h : function.injective f)
{x y : α} :
theorem
right_ord_continuous.lt_iff
{α : Type u}
{β : Type v}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(hf : right_ord_continuous f)
(h : function.injective f)
{x y : α} :
def
right_ord_continuous.to_order_embedding
{α : Type u}
{β : Type v}
[semilattice_inf α]
[semilattice_inf β]
(f : α → β)
(hf : right_ord_continuous f)
(h : function.injective f) :
α ↪o β
Convert an injective left order continuous function to a order_embedding.
Equations
- right_ord_continuous.to_order_embedding f hf h = {to_embedding := {to_fun := f, inj' := h}, map_rel_iff' := _}
@[simp]
theorem
right_ord_continuous.coe_to_order_embedding
{α : Type u}
{β : Type v}
[semilattice_inf α]
[semilattice_inf β]
{f : α → β}
(hf : right_ord_continuous f)
(h : function.injective f) :
⇑(right_ord_continuous.to_order_embedding f hf h) = f
theorem
right_ord_continuous.map_Inf'
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : right_ord_continuous f)
(s : set α) :
f (has_Inf.Inf s) = has_Inf.Inf (f '' s)
theorem
right_ord_continuous.map_Inf
{α : Type u}
{β : Type v}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : right_ord_continuous f)
(s : set α) :
f (has_Inf.Inf s) = ⨅ (x : α) (H : x ∈ s), f x
theorem
right_ord_continuous.map_infi
{α : Type u}
{β : Type v}
{ι : Sort x}
[complete_lattice α]
[complete_lattice β]
{f : α → β}
(hf : right_ord_continuous f)
(g : ι → α) :
theorem
right_ord_continuous.map_cInf
{α : Type u}
{β : Type v}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{f : α → β}
(hf : right_ord_continuous f)
{s : set α}
(sne : s.nonempty)
(sbdd : bdd_below s) :
f (has_Inf.Inf s) = has_Inf.Inf (f '' s)
theorem
right_ord_continuous.map_cinfi
{α : Type u}
{β : Type v}
{ι : Sort x}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
[nonempty ι]
{f : α → β}
(hf : right_ord_continuous f)
{g : ι → α}
(hg : bdd_below (set.range g)) :