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 β] :
(α → β) → 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 β] :
(α → β) → 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
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 xis_greatest (f '' s) (f x)

theorem left_ord_continuous.mono {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

theorem left_ord_continuous.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {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 : α) :
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 : α → β) :

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 α) :
f (Sup s) = 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 (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.nonemptybdd_above sf (Sup s) = 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 : ι → α} :
bdd_above (set.range g)(f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i))

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 : α} :
is_least s xis_least (f '' s) (f x)

theorem right_ord_continuous.mono {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} :

theorem right_ord_continuous.comp {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {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 : α) :
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 : α → β) :

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 α) :
f (Inf s) = 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 (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.nonemptybdd_below sf (Inf s) = 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 : ι → α} :
bdd_below (set.range g)(f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i))

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 β) :