Documentation

Mathlib.Topology.OmegaCompletePartialOrder

Scott Topological Spaces #

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

Reference #

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

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

Equations
Instances For
    def Scott.IsOpen (α : Type u) [OmegaCompletePartialOrder α] (s : Set α) :

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

    Equations
    Instances For
      theorem Scott.IsOpen.inter (α : Type u) [OmegaCompletePartialOrder α] (s : Set α) (t : Set α) :
      Scott.IsOpen α sScott.IsOpen α tScott.IsOpen α (s t)
      theorem Scott.isOpen_sUnion (α : Type u) [OmegaCompletePartialOrder α] (s : Set (Set α)) (hs : ts, Scott.IsOpen α t) :
      @[reducible, inline]
      abbrev Scott (α : 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
        Equations
        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