# Documentation

Mathlib.Order.OrdContinuous

# 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 a RelIso is both left and right order continuous.

### Definitions #

def LeftOrdContinuous {α : Type u} {β : Type v} [inst : ] [inst : ] (f : αβ) :

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 RightOrdContinuous {α : Type u} {β : Type v} [inst : ] [inst : ] (f : αβ) :

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 LeftOrdContinuous.id (α : Type u) [inst : ] :
theorem LeftOrdContinuous.order_dual {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} :
RightOrdContinuous (OrderDual.toDual f OrderDual.ofDual)
theorem LeftOrdContinuous.map_isGreatest {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set α} {x : α} (h : ) :
IsGreatest (f '' s) (f x)
theorem LeftOrdContinuous.mono {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) :
theorem LeftOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [inst : ] [inst : ] [inst : ] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem LeftOrdContinuous.iterate {α : Type u} [inst : ] {f : αα} (hf : ) (n : ) :
theorem LeftOrdContinuous.map_sup {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem LeftOrdContinuous.le_iff {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x f y x y
theorem LeftOrdContinuous.lt_iff {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x < f y x < y
def LeftOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [inst : ] [inst : ] (f : αβ) (hf : ) (h : ) :
α ↪o β

Convert an injective left order continuous function to an order embedding.

Equations
• = { toEmbedding := { toFun := f, inj' := h }, map_rel_iff' := (_ : ∀ {a b : α}, f a f b a b) }
@[simp]
theorem LeftOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) :
().toEmbedding = f
theorem LeftOrdContinuous.map_supₛ' {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (s : Set α) :
f (supₛ s) = supₛ (f '' s)
theorem LeftOrdContinuous.map_supₛ {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (s : Set α) :
f (supₛ s) = x, h, f x
theorem LeftOrdContinuous.map_supᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ] [inst : ] {f : αβ} (hf : ) (g : ια) :
f (i, g i) = i, f (g i)
theorem LeftOrdContinuous.map_csupₛ {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set α} (sne : ) (sbdd : ) :
f (supₛ s) = supₛ (f '' s)
theorem LeftOrdContinuous.map_csupᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ] [inst : ] [inst : ] {f : αβ} (hf : ) {g : ια} (hg : ) :
f (i, g i) = i, f (g i)
theorem RightOrdContinuous.id (α : Type u) [inst : ] :
theorem RightOrdContinuous.orderDual {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} :
LeftOrdContinuous (OrderDual.toDual f OrderDual.ofDual)
theorem RightOrdContinuous.map_isLeast {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set α} {x : α} (h : IsLeast s x) :
IsLeast (f '' s) (f x)
theorem RightOrdContinuous.mono {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) :
theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [inst : ] [inst : ] [inst : ] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem RightOrdContinuous.iterate {α : Type u} [inst : ] {f : αα} (hf : ) (n : ) :
theorem RightOrdContinuous.map_inf {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem RightOrdContinuous.le_iff {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x f y x y
theorem RightOrdContinuous.lt_iff {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x < f y x < y
def RightOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [inst : ] [inst : ] (f : αβ) (hf : ) (h : ) :
α ↪o β

Convert an injective left order continuous function to a order_embedding.

Equations
• = { toEmbedding := { toFun := f, inj' := h }, map_rel_iff' := (_ : ∀ {a b : α}, f a f b a b) }
@[simp]
theorem RightOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (h : ) :
().toEmbedding = f
theorem RightOrdContinuous.map_infₛ' {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (s : Set α) :
f (infₛ s) = infₛ (f '' s)
theorem RightOrdContinuous.map_infₛ {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) (s : Set α) :
f (infₛ s) = x, h, f x
theorem RightOrdContinuous.map_infᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ] [inst : ] {f : αβ} (hf : ) (g : ια) :
f (i, g i) = i, f (g i)
theorem RightOrdContinuous.map_cinfₛ {α : Type u} {β : Type v} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set α} (sne : ) (sbdd : ) :
f (infₛ s) = infₛ (f '' s)
theorem RightOrdContinuous.map_cinfᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ] [inst : ] [inst : ] {f : αβ} (hf : ) {g : ια} (hg : ) :
f (i, g i) = i, f (g i)
theorem OrderIso.leftOrdContinuous {α : Type u} {β : Type v} [inst : ] [inst : ] (e : α ≃o β) :
LeftOrdContinuous ().toEmbedding
theorem OrderIso.rightOrdContinuous {α : Type u} {β : Type v} [inst : ] [inst : ] (e : α ≃o β) :
RightOrdContinuous ().toEmbedding