Exercise 1.14 (Scott 1981, PRG-19, §1) — finite non-empty subsets of ℕ

Let Δ = ℕ and take as neighbourhoods the finite non-empty subsets of ℕ, together with Δ itself. This is the infinite analogue of Example 1.5 (where Δ was finite).

Deliverables:

• neighborhoodSystem : NeighborhoodSystem ℕ — "Show that this is a neighbourhood system." Unlike the tail/binary examples this is not nested-or-disjoint (two finite sets may overlap partially), so condition (ii) is checked by hand: the consistency witness Z ⊆ X ∩ Y keeps X ∩ Y non-empty, and X ∩ Y is finite as soon as either factor is.
• Finite elements. fin h = ↑X (the principal filters), Scott's finite elements.
• Total elements. "What are the total elements?" The maximal filters are exactly the principals of singletons: singleton_isTotal shows ↑{n} is total (a filter strictly above it would have to contain a set missing n, forcing ∅ ∈ 𝒟).

Constructive ([propext, Quot.sound]).

def Domain.Neighborhood.Exercise114.mem (X : Set ℕ) : Prop

Membership: X is a neighbourhood iff X = ℕ (the master Δ) or X is finite and non-empty.

Equations

• Domain.Neighborhood.Exercise114.mem X = (X = Set.univ ∨ X.Finite ∧ X.Nonempty)

theorem Domain.Neighborhood.Exercise114.empty_not_mem : ¬mem ∅

theorem Domain.Neighborhood.Exercise114.nonempty_of_mem {X : Set ℕ} (h : mem X) : X.Nonempty

theorem Domain.Neighborhood.Exercise114.mem_singleton (n : ℕ) : mem {n}

def Domain.Neighborhood.Exercise114.neighborhoodSystem : NeighborhoodSystem ℕ

Exercise 1.14. The neighbourhood system of finite non-empty subsets of ℕ (plus Δ = ℕ).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise114.ns_mem {X : Set ℕ} : neighborhoodSystem.mem X ↔ mem X

Finite elements (principals) and total elements (singletons).

def Domain.Neighborhood.Exercise114.fin {X : Set ℕ} (h : neighborhoodSystem.mem X) : neighborhoodSystem.Element

The finite element ↑X for a neighbourhood X (Scott's finite elements).

Equations

• Domain.Neighborhood.Exercise114.fin h = Domain.Neighborhood.Exercise114.neighborhoodSystem.principal h

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

⊥ = ↑Δ = ↑ℕ, the least element.

Equations

• Domain.Neighborhood.Exercise114.bot = Domain.Neighborhood.Exercise114.neighborhoodSystem.bot

theorem Domain.Neighborhood.Exercise114.singleton_isTotal (n : ℕ) : neighborhoodSystem.IsTotal (neighborhoodSystem.principal ⋯)

Exercise 1.14 (total elements). The principal filter of a singleton {n} is a total (maximal) element: any y it approximates approximates it back. (A y ⊋ ↑{n} would contain some W ∌ n; then {n} ∩ W = ∅ ∈ y ⊆ 𝒟, impossible.) These are exactly the total elements.