Documentation

Mathlib.Topology.OmegaCompletePartialOrder

Scott Topological Spaces #

A type of topological spaces whose notion of continuity is equivalent to continuity in ωCPOs.

Reference #

source
def Scott.IsωSup {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) (x : α) :
Prop

x is an ω-Sup of a chain c if it is the least upper bound of the range of c.

Equations
Instances For
    source
    theorem Scott.isωSup_iff_isLUB {α : Type u} [Preorder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} :
    Scott.IsωSup c x ↔ IsLUB (Set.range ⇑c) x
    source
    def Scott.IsOpen (α : Type u) [OmegaCompletePartialOrder α] (s : Set α) :
    Prop

    The characteristic function of open sets is monotone and preserves the limits of chains.

    Equations
    Instances For
      source
      theorem Scott.isOpen_univ (α : Type u) [OmegaCompletePartialOrder α] :
      Scott.IsOpen α Set.univ
      source
      theorem Scott.IsOpen.inter (α : Type u) [OmegaCompletePartialOrder α] (s : Set α) (t : Set α) :
      Scott.IsOpen α s → Scott.IsOpen α t → Scott.IsOpen α (s ∩ t)
      source
      theorem Scott.isOpen_sUnion (α : Type u) [OmegaCompletePartialOrder α] (s : Set (Set α)) (hs : ∀ t ∈ s, Scott.IsOpen α t) :
      Scott.IsOpen α (⋃₀ s)
      source
      theorem Scott.IsOpen.isUpperSet (α : Type u) [OmegaCompletePartialOrder α] {s : Set α} (hs : Scott.IsOpen α s) :
      IsUpperSet s
      source
      @[reducible]
      def Scott (α : Type u) :
      Type u

      A Scott topological space is defined on preorders such that their open sets, seen as a function α → Prop, preserves the joins of ω-chains

      Equations
      Instances For
        source
        instance Scott.topologicalSpace (α : Type u) [OmegaCompletePartialOrder α] :
        TopologicalSpace (Scott α)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def notBelow {α : Type u_1} [OmegaCompletePartialOrder α] (y : Scott α) :
        Set (Scott α)

        notBelow is an open set in Scott α used to prove the monotonicity of continuous functions

        Equations
        Instances For
          source
          theorem notBelow_isOpen {α : Type u_1} [OmegaCompletePartialOrder α] (y : Scott α) :
          IsOpen (notBelow y)
          source
          theorem isωSup_ωSup {α : Type u_1} [OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) :
          Scott.IsωSup c (OmegaCompletePartialOrder.ωSup c)
          source
          theorem scottContinuous_of_continuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : Continuous f) :
          OmegaCompletePartialOrder.Continuous' f
          source
          theorem continuous_of_scottContinuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : OmegaCompletePartialOrder.Continuous' f) :
          Continuous f