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} [Preorder α] [Preorder β] (f : α → β) : Prop

A function f between preorders is left order continuous if it preserves all suprema of nonempty sets. 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 : α⦄, s.Nonempty → IsLUB s x → IsLUB (f '' s) (f x)

def RightOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) : Prop

A function f between preorders is right order continuous if it preserves all infima of nonempty sets. 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 : α⦄, s.Nonempty → IsGLB s x → IsGLB (f '' s) (f x)

theorem LeftOrdContinuous.id (α : Type u) [Preorder α] : LeftOrdContinuous id

theorem RightOrdContinuous.id (α : Type u) [Preorder α] : RightOrdContinuous id

theorem LeftOrdContinuous.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : LeftOrdContinuous f → RightOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

theorem RightOrdContinuous.dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

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)

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)

theorem LeftOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : LeftOrdContinuous f) : Monotone f

theorem RightOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : RightOrdContinuous f) : Monotone f

theorem LeftOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : LeftOrdContinuous g) (hf : LeftOrdContinuous f) : LeftOrdContinuous (g ∘ f)

theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : β → γ} {f : α → β} (hg : RightOrdContinuous g) (hf : RightOrdContinuous f) : RightOrdContinuous (g ∘ f)

theorem LeftOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : LeftOrdContinuous f) (n : ℕ) : LeftOrdContinuous f^[n]

theorem RightOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : RightOrdContinuous f) (n : ℕ) : RightOrdContinuous f^[n]

theorem LeftOrdContinuous.map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (x y : α) : f (x ⊔ y) = f x ⊔ f y

theorem RightOrdContinuous.map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (x y : α) : f (x ⊓ y) = f x ⊓ f y

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

theorem RightOrdContinuous.le_iff {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) {x y : α} : f y ≤ f x ↔ y ≤ x

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

theorem RightOrdContinuous.lt_iff {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) {x y : α} : f y < f x ↔ y < x

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' := ⋯ }

def RightOrdContinuous.toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] (f : α → β) (hf : RightOrdContinuous f) (h : Function.Injective f) : α ↪o β

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

Equations

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

@[simp]

theorem LeftOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (h : Function.Injective f) : ⇑(toOrderEmbedding f hf h) = f

@[simp]

theorem RightOrdContinuous.coe_toOrderEmbedding {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) : ⇑(toOrderEmbedding f hf h) = f

theorem LeftOrdContinuous.map_sSup' {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) {s : Set α} (hs : s.Nonempty) : f (sSup s) = sSup (f '' s)

theorem RightOrdContinuous.map_sInf' {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) {s : Set α} (hs : s.Nonempty) : f (sInf s) = sInf (f '' s)

theorem LeftOrdContinuous.map_sSup {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) {s : Set α} (hs : s.Nonempty) : f (sSup s) = ⨆ x ∈ s, f x

theorem RightOrdContinuous.map_sInf {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) {s : Set α} (hs : s.Nonempty) : f (sInf s) = ⨅ x ∈ s, f x

theorem LeftOrdContinuous.map_iSup {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) [Nonempty ι] (g : ι → α) : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

theorem RightOrdContinuous.map_iInf {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) [Nonempty ι] (g : ι → α) : f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)

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)

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)

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)

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)

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.

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.

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

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