# 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 #

source
def LeftOrdContinuous {α : 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 `IsLUB` instead of `sSup` so that the proof works both for complete lattices and conditionally complete lattices.

Equations

- LeftOrdContinuous f = ∀ ⦃s : Set α⦄ ⦃x : α⦄, IsLUB s x → IsLUB (f '' s) (f x)

Instances For

source
def RightOrdContinuous {α : 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 `IsGLB` instead of `sInf` so that the proof works both for complete lattices and conditionally complete lattices.

Equations

- RightOrdContinuous f = ∀ ⦃s : Set α⦄ ⦃x : α⦄, IsGLB s x → IsGLB (f '' s) (f x)

Instances For

source
theorem LeftOrdContinuous.id (α : Type u) [Preorder α] :
LeftOrdContinuous id
source
theorem LeftOrdContinuous.rightOrdContinuous_dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :
LeftOrdContinuous f → RightOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
source
theorem LeftOrdContinuous.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : LeftOrdContinuous f) {s : Set α} {x : α} (h : IsGreatest s x) :
IsGreatest (f '' s) (f x)
source
theorem LeftOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : LeftOrdContinuous f) :
Monotone f
source
theorem LeftOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : LeftOrdContinuous g) (hf : LeftOrdContinuous f) :
LeftOrdContinuous (g ∘ f)
source
theorem LeftOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : LeftOrdContinuous f) (n : ℕ) :
LeftOrdContinuous f^[n]
source
theorem LeftOrdContinuous.map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (x y : α) :
f (x ⊔ y) = f x ⊔ f y
source
theorem LeftOrdContinuous.le_iff {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (h : Function.Injective f) {x y : α} :
f x ≤ f y ↔ x ≤ y
source
theorem LeftOrdContinuous.lt_iff {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (h : Function.Injective f) {x y : α} :
f x < f y ↔ x < y
source
def LeftOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] (f : α → β) (hf : LeftOrdContinuous f) (h : Function.Injective f) :
α ↪o β

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

Equations

- LeftOrdContinuous.toOrderEmbedding f hf h = { toFun := f, inj' := h, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem LeftOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (h : Function.Injective f) :
⇑(toOrderEmbedding f hf h) = f
source
theorem LeftOrdContinuous.map_sSup' {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) (s : Set α) :
f (sSup s) = sSup (f '' s)
source
theorem LeftOrdContinuous.map_sSup {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) (s : Set α) :
f (sSup s) = ⨆ x ∈ s, f x
source
theorem LeftOrdContinuous.map_iSup {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) (g : ι → α) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem LeftOrdContinuous.map_csSup {α : Type u} {β : Type v} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) {s : Set α} (sne : s.Nonempty) (sbdd : BddAbove s) :
f (sSup s) = sSup (f '' s)
source
theorem LeftOrdContinuous.map_ciSup {α : Type u} {β : Type v} {ι : Sort x} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {f : α → β} (hf : LeftOrdContinuous f) {g : ι → α} (hg : BddAbove (Set.range g)) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem RightOrdContinuous.id (α : Type u) [Preorder α] :
RightOrdContinuous id
source
theorem RightOrdContinuous.orderDual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} :
RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
source
theorem RightOrdContinuous.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : RightOrdContinuous f) {s : Set α} {x : α} (h : IsLeast s x) :
IsLeast (f '' s) (f x)
source
theorem RightOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : RightOrdContinuous f) :
Monotone f
source
theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : RightOrdContinuous g) (hf : RightOrdContinuous f) :
RightOrdContinuous (g ∘ f)
source
theorem RightOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : RightOrdContinuous f) (n : ℕ) :
RightOrdContinuous f^[n]
source
theorem RightOrdContinuous.map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (x y : α) :
f (x ⊓ y) = f x ⊓ f y
source
theorem RightOrdContinuous.le_iff {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) {x y : α} :
f x ≤ f y ↔ x ≤ y
source
theorem RightOrdContinuous.lt_iff {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) {x y : α} :
f x < f y ↔ x < y
source
def RightOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] (f : α → β) (hf : RightOrdContinuous f) (h : Function.Injective f) :
α ↪o β

Convert an injective left order continuous function to an `OrderEmbedding`.

Equations

- RightOrdContinuous.toOrderEmbedding f hf h = { toFun := f, inj' := h, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem RightOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) :
⇑(toOrderEmbedding f hf h) = f
source
theorem RightOrdContinuous.map_sInf' {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) (s : Set α) :
f (sInf s) = sInf (f '' s)
source
theorem RightOrdContinuous.map_sInf {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) (s : Set α) :
f (sInf s) = ⨅ x ∈ s, f x
source
theorem RightOrdContinuous.map_iInf {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) (g : ι → α) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
source
theorem RightOrdContinuous.map_csInf {α : Type u} {β : Type v} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) {s : Set α} (sne : s.Nonempty) (sbdd : BddBelow s) :
f (sInf s) = sInf (f '' s)
source
theorem RightOrdContinuous.map_ciInf {α : Type u} {β : Type v} {ι : Sort x} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {f : α → β} (hf : RightOrdContinuous f) {g : ι → α} (hg : BddBelow (Set.range g)) :
f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)
source
theorem GaloisConnection.leftOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {g : β → α} (gc : GaloisConnection f g) :
LeftOrdContinuous f

A left adjoint in a Galois connection is left-continuous in the order-theoretic sense.

source
theorem GaloisConnection.rightOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {g : β → α} (gc : GaloisConnection f g) :
RightOrdContinuous g

A right adjoint in a Galois connection is right-continuous in the order-theoretic sense.

source
theorem OrderIso.leftOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) :
LeftOrdContinuous ⇑e
source
theorem OrderIso.rightOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) :
RightOrdContinuous ⇑e