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} [Preorder α] [Preorder β] (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.

Equations
Instances For
    def RightOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (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.

    Equations
    Instances For
      theorem LeftOrdContinuous.order_dual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} :
      LeftOrdContinuous fRightOrdContinuous (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) :
      theorem LeftOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} (hg : LeftOrdContinuous g) (hf : LeftOrdContinuous f) :
      theorem LeftOrdContinuous.iterate {α : Type u} [Preorder α] {f : αα} (hf : 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
      Instances For
        @[simp]
        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) = xs, 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 : s.Nonempty) (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.orderDual {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} :
        RightOrdContinuous fLeftOrdContinuous (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) :
        theorem RightOrdContinuous.comp {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} (hg : RightOrdContinuous g) (hf : RightOrdContinuous f) :
        theorem RightOrdContinuous.iterate {α : Type u} [Preorder α] {f : αα} (hf : 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
        Instances For
          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) = xs, 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 : s.Nonempty) (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 β) :
          theorem OrderIso.rightOrdContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) :