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

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

Equations
@[simp]
theorem LeftOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst : SemilatticeSup β] {f : αβ} (hf : LeftOrdContinuous f) (h : Function.Injective f) :
(LeftOrdContinuous.toOrderEmbedding f hf h).toEmbedding = f
theorem LeftOrdContinuous.map_supₛ' {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : LeftOrdContinuous f) (s : Set α) :
f (supₛ s) = supₛ (f '' s)
theorem LeftOrdContinuous.map_supₛ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : LeftOrdContinuous f) (s : Set α) :
f (supₛ s) = x, h, f x
theorem LeftOrdContinuous.map_supᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : LeftOrdContinuous f) (g : ια) :
f (i, g i) = i, f (g i)
theorem LeftOrdContinuous.map_csupₛ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {f : αβ} (hf : LeftOrdContinuous f) {s : Set α} (sne : Set.Nonempty s) (sbdd : BddAbove s) :
f (supₛ s) = supₛ (f '' s)
theorem LeftOrdContinuous.map_csupᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] {f : αβ} (hf : LeftOrdContinuous f) {g : ια} (hg : BddAbove (Set.range g)) :
f (i, g i) = i, f (g i)
theorem RightOrdContinuous.orderDual {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} :
RightOrdContinuous fLeftOrdContinuous (OrderDual.toDual f OrderDual.ofDual)
theorem RightOrdContinuous.map_isLeast {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (hf : RightOrdContinuous f) {s : Set α} {x : α} (h : IsLeast s x) :
IsLeast (f '' s) (f x)
theorem RightOrdContinuous.mono {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] {f : αβ} (hf : RightOrdContinuous f) :
theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {g : βγ} {f : αβ} (hg : RightOrdContinuous g) (hf : RightOrdContinuous f) :
theorem RightOrdContinuous.iterate {α : Type u} [inst : Preorder α] {f : αα} (hf : RightOrdContinuous f) (n : ) :
theorem RightOrdContinuous.map_inf {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : SemilatticeInf β] {f : αβ} (hf : RightOrdContinuous f) (x : α) (y : α) :
f (x y) = f x f y
theorem RightOrdContinuous.le_iff {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : SemilatticeInf β] {f : αβ} (hf : RightOrdContinuous f) (h : Function.Injective f) {x : α} {y : α} :
f x f y x y
theorem RightOrdContinuous.lt_iff {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : SemilatticeInf β] {f : αβ} (hf : RightOrdContinuous f) (h : Function.Injective f) {x : α} {y : α} :
f x < f y x < y
def RightOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : SemilatticeInf β] (f : αβ) (hf : RightOrdContinuous f) (h : Function.Injective f) :
α ↪o β

Convert an injective left order continuous function to a order_embedding.

Equations
@[simp]
theorem RightOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst : SemilatticeInf β] {f : αβ} (hf : RightOrdContinuous f) (h : Function.Injective f) :
(RightOrdContinuous.toOrderEmbedding f hf h).toEmbedding = f
theorem RightOrdContinuous.map_infₛ' {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : RightOrdContinuous f) (s : Set α) :
f (infₛ s) = infₛ (f '' s)
theorem RightOrdContinuous.map_infₛ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : RightOrdContinuous f) (s : Set α) :
f (infₛ s) = x, h, f x
theorem RightOrdContinuous.map_infᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : RightOrdContinuous f) (g : ια) :
f (i, g i) = i, f (g i)
theorem RightOrdContinuous.map_cinfₛ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] {f : αβ} (hf : RightOrdContinuous f) {s : Set α} (sne : Set.Nonempty s) (sbdd : BddBelow s) :
f (infₛ s) = infₛ (f '' s)
theorem RightOrdContinuous.map_cinfᵢ {α : Type u} {β : Type v} {ι : Sort x} [inst : ConditionallyCompleteLattice α] [inst : ConditionallyCompleteLattice β] [inst : Nonempty ι] {f : αβ} (hf : RightOrdContinuous f) {g : ια} (hg : BddBelow (Set.range g)) :
f (i, g i) = i, f (g i)
theorem OrderIso.leftOrdContinuous {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (e : α ≃o β) :
theorem OrderIso.rightOrdContinuous {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (e : α ≃o β) :