Documentation

Mathlib.Topology.OmegaCompletePartialOrder

Scott Topological Spaces #

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

Reference #

source
@[simp]
theorem Topology.IsScott.ωScottContinuous_iff_continuous {α : Type u_1} [OmegaCompletePartialOrder α] [TopologicalSpace α] [IsScott α (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c)] {f : α → Prop} :
OmegaCompletePartialOrder.ωScottContinuous f ↔ Continuous f
source
@[deprecated Topology.IsScott.ωScottContinuous_iff_continuous (since := "2025-07-02")]
theorem Topology.IsScott.ωscottContinuous_iff_continuous {α : Type u_1} [OmegaCompletePartialOrder α] [TopologicalSpace α] [IsScott α (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c)] {f : α → Prop} :
OmegaCompletePartialOrder.ωScottContinuous f ↔ Continuous f

Alias of Topology.IsScott.ωScottContinuous_iff_continuous.

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 : α} :
      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 α] :
          IsOpen α Set.univ
          source
          theorem Scott.IsOpen.inter (α : Type u) [OmegaCompletePartialOrder α] (s t : Set α) :
          IsOpen α s → IsOpen α t → IsOpen α (s ∩ t)
          source
          theorem Scott.isOpen_sUnion (α : Type u) [OmegaCompletePartialOrder α] (s : Set (Set α)) (hs : ∀ t ∈ s, IsOpen α t) :
          IsOpen α (⋃₀ s)
          source
          theorem Scott.IsOpen.isUpperSet (α : Type u) [OmegaCompletePartialOrder α] {s : Set α} (hs : IsOpen α s) :
          IsUpperSet s
          source
          @[reducible, inline, deprecated Topology.WithScott (since := "2025-07-02")]
          abbrev 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
              @[reducible, inline, deprecated Topology.WithScott.instTopologicalSpace (since := "2025-07-02")]
              abbrev Scott.topologicalSpace (α : Type u) [OmegaCompletePartialOrder α] :
              TopologicalSpace (Scott α)

              Deprecated, use WithScott.

              Equations
                Instances For
                  source
                  @[deprecated isOpen_iff_continuous_mem (since := "2025-07-02")]
                  theorem isOpen_iff_ωScottContinuous_mem {α : Type u_1} [OmegaCompletePartialOrder α] {s : Set (Scott α)} :
                  IsOpen s ↔ OmegaCompletePartialOrder.ωScottContinuous fun (x : Scott α) => x ∈ s
                  source
                  @[deprecated "Use `WithScott` API" (since := "2025-07-02")]
                  theorem scott_eq_Scott {α : Type u_1} [OmegaCompletePartialOrder α] :
                  Topology.scott α (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c) = Scott.topologicalSpace α
                  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
                      @[deprecated isClosed_Iic (since := "2025-07-02")]
                      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
                      @[deprecated Topology.IsScott.ωscottContinuous_iff_continuous (since := "2025-07-02")]
                      theorem scottContinuous_of_continuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : Continuous f) :
                      OmegaCompletePartialOrder.ωScottContinuous f
                      source
                      @[deprecated Topology.IsScott.ωscottContinuous_iff_continuous (since := "2025-07-02")]
                      theorem continuous_of_scottContinuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : OmegaCompletePartialOrder.ωScottContinuous f) :
                      Continuous f