Example 1.2 (Scott 1981, PRG-19, §1)

Scott's first worked example: tokens Δ = {0, 1} and neighbourhoods 𝒟 = {{0, 1}, {0}, {1}}.

We construct the neighbourhood system, prove it satisfies Definition 1.1, and classify its domain elements (Definition 1.6): there are exactly three filters, and exactly one partial element — the bottom filter {Δ}.

@[reducible, inline]

abbrev Domain.Neighborhood.Example12.Token : Type

Tokens for Example 1.2: Δ = {0, 1}.

Equations

• Domain.Neighborhood.Example12.Token = Fin 2

def Domain.Neighborhood.Example12.master : Set Token

The master neighbourhood Δ = {0, 1}.

Equations

• Domain.Neighborhood.Example12.master = Set.univ

def Domain.Neighborhood.Example12.zero : Set Token

The neighbourhood {0}.

Equations

• Domain.Neighborhood.Example12.zero = {0}

def Domain.Neighborhood.Example12.one : Set Token

The neighbourhood {1}.

Equations

• Domain.Neighborhood.Example12.one = {1}

def Domain.Neighborhood.Example12.memSet : Set (Set Token)

The three neighbourhoods of Example 1.2.

Equations

• Domain.Neighborhood.Example12.memSet = {Domain.Neighborhood.Example12.master, Domain.Neighborhood.Example12.zero, Domain.Neighborhood.Example12.one}

def Domain.Neighborhood.Example12.mem (X : Set Token) : Prop

Membership in the neighbourhood system 𝒟 of Example 1.2.

Equations

• Domain.Neighborhood.Example12.mem X = (X ∈ Domain.Neighborhood.Example12.memSet)

theorem Domain.Neighborhood.Example12.mem_master : mem master

theorem Domain.Neighborhood.Example12.mem_zero : mem zero

theorem Domain.Neighborhood.Example12.mem_one : mem one

theorem Domain.Neighborhood.Example12.mem_iff (X : Set Token) : mem X ↔ X = master ∨ X = zero ∨ X = one

A neighbourhood of Example 1.2 is exactly one of Δ, {0}, or {1}.

theorem Domain.Neighborhood.Example12.not_mem_empty : ¬mem ∅

def Domain.Neighborhood.Example12.neighborhoodSystem : NeighborhoodSystem Token

Example 1.2. The neighbourhood system on Δ = {0, 1}.

Equations

• One or more equations did not get rendered due to their size.

def Domain.Neighborhood.Example12.neighborhoodSystem.bot : neighborhoodSystem.Element

The bottom element ⊥ = {Δ}.

Equations

• One or more equations did not get rendered due to their size.

def Domain.Neighborhood.Example12.neighborhoodSystem.elemZero : neighborhoodSystem.Element

The total element determined by {0}.

Equations

• One or more equations did not get rendered due to their size.

def Domain.Neighborhood.Example12.neighborhoodSystem.elemOne : neighborhoodSystem.Element

The total element determined by {1}.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Example12.neighborhoodSystem.element_classification (x : neighborhoodSystem.Element) : x = bot ∨ x = elemZero ∨ x = elemOne

Every element of Example 1.2 is one of the three filters ⊥, {0}-total, {1}-total.

theorem Domain.Neighborhood.Example12.neighborhoodSystem.bot_lt_elemZero : bot < elemZero

The bottom filter is the only partial element: it is strictly below both total elements.

theorem Domain.Neighborhood.Example12.neighborhoodSystem.bot_lt_elemOne : bot < elemOne

theorem Domain.Neighborhood.Example12.neighborhoodSystem.bot_is_unique_partial (x : neighborhoodSystem.Element) : x ≠ elemZero → x ≠ elemOne → x = bot