Order continuity
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.
theorem
left_ord_continuous.order_dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β} :
theorem
left_ord_continuous.map_is_greatest
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : left_ord_continuous f)
{s : set α}
{x : α} :
is_greatest s x → is_greatest (f '' s) (f x)
theorem
left_ord_continuous.mono
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β} :
left_ord_continuous f → monotone f
theorem
left_ord_continuous.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β} :
left_ord_continuous g → left_ord_continuous f → left_ord_continuous (g ∘ f)
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 : α → β) :
left_ord_continuous f → 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 : ι → α) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
theorem
left_ord_continuous.map_cSup
{α : Type u}
{β : Type v}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{f : α → β}
(hf : left_ord_continuous f)
{s : set α} :
s.nonempty → 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 : ι → α} :
theorem
right_ord_continuous.order_dual
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β} :
theorem
right_ord_continuous.map_is_least
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β}
(hf : right_ord_continuous f)
{s : set α}
{x : α} :
theorem
right_ord_continuous.mono
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
{f : α → β} :
right_ord_continuous f → monotone f
theorem
right_ord_continuous.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder α]
[preorder β]
[preorder γ]
{g : β → γ}
{f : α → β} :
right_ord_continuous g → right_ord_continuous f → right_ord_continuous (g ∘ f)
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 : α → β) :
right_ord_continuous f → 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 : ι → α) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
theorem
right_ord_continuous.map_cInf
{α : Type u}
{β : Type v}
[conditionally_complete_lattice α]
[conditionally_complete_lattice β]
{f : α → β}
(hf : right_ord_continuous f)
{s : set α} :
s.nonempty → 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 : ι → α} :
theorem
order_iso.left_ord_continuous
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(e : α ≃o β) :
theorem
order_iso.right_ord_continuous
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(e : α ≃o β) :