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

Scott's fourth worked example: tokens Δ = {0, 1, 2, 3} and 𝒟 the family of all non-empty subsets of Δ.

This system is a direct generalization of Example 1.2 … The verification that the present 𝒟 is a neighbourhood system rests on nothing more than the remark that sets are consistent in 𝒟 iff they have a non-empty intersection.

We encode tokens as Fin 4, take mem X := X.Nonempty, and master := Set.univ. Condition (ii) of Definition 1.1 is immediate: a consistency witness Z ⊆ X ∩ Y that is itself non-empty makes X ∩ Y non-empty.

• Example 1.5 — neighborhoodSystem.
• Factoid 1.5a — consistent_iff_inter_nonempty: a finite prefix is consistent in 𝒟 iff its intersection is non-empty (Scott's "remark").

Unlike Examples 1.2–1.4 this construction needs no fin_cases/decide: it is Set.Nonempty bookkeeping, so it audits constructive ([propext, Quot.sound]).

@[reducible, inline]

abbrev Domain.Neighborhood.Example15.Token : Type

Tokens for Example 1.5: Δ = {0, 1, 2, 3}.

Equations

• Domain.Neighborhood.Example15.Token = Fin 4

def Domain.Neighborhood.Example15.master : Set Token

The master neighbourhood Δ = {0, 1, 2, 3}.

Equations

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

def Domain.Neighborhood.Example15.neighborhoodSystem : NeighborhoodSystem Token

Example 1.5. The neighbourhood system of all non-empty subsets of Δ = {0,1,2,3}.

Equations

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

theorem Domain.Neighborhood.Example15.mem_iff_nonempty (X : Set Token) : neighborhoodSystem.mem X ↔ X.Nonempty

The neighbourhoods of Example 1.5 are exactly the non-empty subsets.

theorem Domain.Neighborhood.Example15.consistent_iff_inter_nonempty (X : ℕ → Set Token) (n : ℕ) : neighborhoodSystem.Consistent X n ↔ (neighborhoodSystem.interUpTo X n).Nonempty

Factoid 1.5a (Scott 1981, PRG-19). In Example 1.5, "sets are consistent in 𝒟 iff they have a non-empty intersection": a finite prefix X₀, …, Xₙ₋₁ is consistent exactly when its intersection ⋂_{i<n} Xᵢ is non-empty.