# 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_sSup etc) and prove that a RelIso is both left and right order continuous.

### Definitions #

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

A function f between preorders is left order continuous if it preserves all suprema. We define it using IsLUB instead of sSup so that the proof works both for complete lattices and conditionally complete lattices.

Instances For
def RightOrdContinuous {α : Type u} {β : Type v} [] [] (f : αβ) :

A function f between preorders is right order continuous if it preserves all infima. We define it using IsGLB instead of sInf so that the proof works both for complete lattices and conditionally complete lattices.

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

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

Instances For
@[simp]
theorem LeftOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (h : ) :
↑() = f
theorem LeftOrdContinuous.map_sSup' {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (s : Set α) :
f (sSup s) = sSup (f '' s)
theorem LeftOrdContinuous.map_sSup {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (s : Set α) :
f (sSup s) = ⨆ (x : α) (_ : x s), f x
theorem LeftOrdContinuous.map_iSup {α : Type u} {β : Type v} {ι : Sort x} [] [] {f : αβ} (hf : ) (g : ια) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
theorem LeftOrdContinuous.map_csSup {α : Type u} {β : Type v} {f : αβ} (hf : ) {s : Set α} (sne : ) (sbdd : ) :
f (sSup s) = sSup (f '' s)
theorem LeftOrdContinuous.map_ciSup {α : Type u} {β : Type v} {ι : Sort x} [] {f : αβ} (hf : ) {g : ια} (hg : ) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
theorem RightOrdContinuous.id (α : Type u) [] :
theorem RightOrdContinuous.orderDual {α : Type u} {β : Type v} [] [] {f : αβ} :
LeftOrdContinuous (OrderDual.toDual f OrderDual.ofDual)
theorem RightOrdContinuous.map_isLeast {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) {s : Set α} {x : α} (h : IsLeast s x) :
IsLeast (f '' s) (f x)
theorem RightOrdContinuous.mono {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) :
theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem RightOrdContinuous.iterate {α : Type u} [] {f : αα} (hf : ) (n : ) :
theorem RightOrdContinuous.map_inf {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem RightOrdContinuous.le_iff {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x f y x y
theorem RightOrdContinuous.lt_iff {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (h : ) {x : α} {y : α} :
f x < f y x < y
def RightOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [] [] (f : αβ) (hf : ) (h : ) :
α ↪o β

Convert an injective left order continuous function to an OrderEmbedding.

Instances For
@[simp]
theorem RightOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (h : ) :
↑() = f
theorem RightOrdContinuous.map_sInf' {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (s : Set α) :
f (sInf s) = sInf (f '' s)
theorem RightOrdContinuous.map_sInf {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (s : Set α) :
f (sInf s) = ⨅ (x : α) (_ : x s), f x
theorem RightOrdContinuous.map_iInf {α : Type u} {β : Type v} {ι : Sort x} [] [] {f : αβ} (hf : ) (g : ια) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
theorem RightOrdContinuous.map_csInf {α : Type u} {β : Type v} {f : αβ} (hf : ) {s : Set α} (sne : ) (sbdd : ) :
f (sInf s) = sInf (f '' s)
theorem RightOrdContinuous.map_ciInf {α : Type u} {β : Type v} {ι : Sort x} [] {f : αβ} (hf : ) {g : ια} (hg : ) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
theorem OrderIso.leftOrdContinuous {α : Type u} {β : Type v} [] [] (e : α ≃o β) :
theorem OrderIso.rightOrdContinuous {α : Type u} {β : Type v} [] [] (e : α ≃o β) :