mathlib documentation

order.ord_continuous

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 #

def left_ord_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :
Prop

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.

Equations
def right_ord_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) :
Prop

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.

Equations
@[protected]
theorem left_ord_continuous.id (α : Type u) [preorder α] :
@[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) :
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) :
@[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 : α) :
f (x y) = f x f 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 : α} :
f x f y 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 : α} :
f x < f y 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
@[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) :
theorem left_ord_continuous.map_Sup' {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : α → β} (hf : left_ord_continuous f) (s : set α) :
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 α} (sne : s.nonempty) (sbdd : bdd_above 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)) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
@[protected]
@[protected]
theorem right_ord_continuous.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : right_ord_continuous f) {s : set α} {x : α} (h : is_least s x) :
is_least (f '' s) (f x)
theorem right_ord_continuous.mono {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : right_ord_continuous 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) :
@[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 : α) :
f (x y) = f x f 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 : α} :
f x f y 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 : α} :
f x < f y 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
@[simp]
theorem right_ord_continuous.map_Inf' {α : Type u} {β : Type v} [complete_lattice α] [complete_lattice β] {f : α → β} (hf : right_ord_continuous f) (s : set α) :
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 α} (sne : s.nonempty) (sbdd : bdd_below 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)) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
@[protected]
theorem order_iso.left_ord_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) :
@[protected]
theorem order_iso.right_ord_continuous {α : Type u} {β : Type v} [preorder α] [preorder β] (e : α ≃o β) :