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. 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)

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)

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

theorem LeftOrdContinuous.order_dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} : LeftOrdContinuous f → RightOrdContinuous (⇑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 LeftOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : LeftOrdContinuous 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 LeftOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : LeftOrdContinuous f) (n : ℕ) : LeftOrdContinuous 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 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 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

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 = { 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} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (hf : LeftOrdContinuous f) (h : Function.Injective f) : ⇑(LeftOrdContinuous.toOrderEmbedding f hf h) = f

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

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

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)

theorem LeftOrdContinuous.map_csSup {α : Type u} {β : Type v} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {f : α → β} (hf : LeftOrdContinuous f) {s : Set α} (sne : Set.Nonempty s) (sbdd : BddAbove s) : f (sSup s) = sSup (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.id (α : Type u) [Preorder α] : RightOrdContinuous id

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

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 RightOrdContinuous.mono {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : RightOrdContinuous f) : Monotone 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 RightOrdContinuous.iterate {α : Type u} [Preorder α] {f : α → α} (hf : RightOrdContinuous f) (n : ℕ) : RightOrdContinuous f^[n]

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

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

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

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 = { 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} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (hf : RightOrdContinuous f) (h : Function.Injective f) : ⇑(RightOrdContinuous.toOrderEmbedding f hf h) = f

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

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

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)

theorem RightOrdContinuous.map_csInf {α : Type u} {β : Type v} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {f : α → β} (hf : RightOrdContinuous f) {s : Set α} (sne : Set.Nonempty s) (sbdd : BddBelow s) : f (sInf s) = sInf (f '' s)

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