Scott

This file defines the Scott-topology and its relation to the Cantor-topology.

Main definitions

• 𝒪.scottTopology: The Scott-topology.
• 𝒪: The set of Scott open sets.
• 𝒪.borel: The Borel measurable space generated by the Scott-topology.
• cantor_borel_eq_scott_borel: Theorem relating the Borel sets generated by the Cantor- and the Scott-topologies.

instance ProbNetKAT.𝒪.scottTopology {H : Type} : TopologicalSpace (Set H)

Equations

• ProbNetKAT.𝒪.scottTopology = Topology.scott (Set H) Set.univ

def ProbNetKAT.𝒪.borel {H : Type} : MeasurableSpace (Set H)

The Borel measurable space generated by the Scott-topology.

Equations

• ProbNetKAT.𝒪.borel = borel (Set H)

def ProbNetKAT.𝒪 {H : Type} : Set (Set (Set H))

The set of Scott-open sets.

Equations

• ProbNetKAT.𝒪 = TopologicalSpace.IsOpen

instance ProbNetKAT.𝒪.IsScott {H : Type} : Topology.IsScott (Set H) Set.univ

theorem ProbNetKAT.𝒪_IsPiSystem {H : Type} : IsPiSystem 𝒪

The Scott-open sets are a Pi-system, i.e. closed under intersection.

theorem ProbNetKAT.𝒪_mem_iff_finite_cover {H : Type} (B : Set (Set H)) : B ∈ 𝒪 ↔ ∃ F ⊆ ℘ω Set.univ, B = ⋃ a ∈ F, B{a}

Lemma 6. A subset B ⊆ 2H is Scott-open iff there exists F ⊆ ℘ω(H) such that B = ⋃ a ∈ F, B{a}.

@[simp]

theorem ProbNetKAT.B_h_is_scott_open {H : Type} {q : H} : B[q] ∈ 𝒪

@[simp]

theorem ProbNetKAT.B_h_is_scott_measurable {α✝ : Type} {q : α✝} : MeasurableSet B[q]

theorem ProbNetKAT.ahsjkdas {H : Type} (B : Set (Set H)) (hB : B ∈ 𝒪) : ∃ A ⊆ ℘ω Set.univ, B = ⋃ a ∈ A, B{a}

Every open set is a countable union of basic open sets B{a}, a ∈ ℘ω(H).

theorem ProbNetKAT.cantor_borel_eq_scott_borel {H : Type} : ℬ.borel = 𝒪.borel

The Borel sets of the two topologies (Cantor and Scott) are the same.