Exercise 2.20 (Scott 1981, PRG-19, §2) — the powerset domain 𝒫

EXERCISE 2.20. Discuss again the example of Exercise 1.15 where the domain turns out to be the powerset of ℕ. Show how the finite elements can be taken to be the finite subsets of ℕ and can be identified with the tokens of a suitable neighbourhood system 𝒫. (Hint: Define ↑F for finite sets F ⊆ ℕ.) Show that both x ∪ y and x ∩ y are approximable functions of two variables, and that x + 1 = {n + 1 ∣ n ∈ x} and x − 1 = {n ∣ n + 1 ∈ x} are approximable.

⚠ Numbering note. Our Exercise115.lean formalized the flat/stem systems, not the powerset domain; so 𝒫 is built fresh here.

Token encoding. We take tokens Δ = ℕ and let the neighbourhoods of 𝒫 be the cofinite subsets of ℕ. Since the principal-filter map X ↦ ↑X is inclusion-reversing, the finite element ↑X represents the finite set Xᶜ; as Xᶜ grows (more elements known to be in the set), the neighbourhood X shrinks (more information). Concretely a finite subset F ⊆ ℕ is the finite element ↑(Fᶜ), and ⊥ = ↑ℕ is the empty set.

• powerSet : NeighborhoodSystem ℕ — cofinite sets (closed under finite ∩).
• toSet x := {n ∣ {n}ᶜ ∈ x} and ofSet S — the identification, packaged as equivSetNat : |𝒫| ≃o (Set ℕ, ⊆) (toSet/ofSet mutually inverse, order-iso).
• unionMap, interMap₂ : ApproximableMap₂ 𝒫 𝒫 𝒫 — x ∪ y, x ∩ y (Exercise 2.19), with toSet_unionMap/toSet_interMap₂ proving the elementwise action is ∪/∩ on Set ℕ.
• succMap, predMap : ApproximableMap 𝒫 𝒫 — x + 1, x − 1, with toSet_succMap/toSet_predMap.

Choice-free (#print axioms ⊆ {propext, Quot.sound}); the Set.Finite.induction_on in mem_compl_of_finite is structural recursion on a finiteness proof, not Classical.choice.

The neighbourhood system 𝒫 (cofinite sets).

def Domain.Neighborhood.Exercise220.powerSet : NeighborhoodSystem ℕ

Exercise 2.20 — the powerset system 𝒫. Tokens ℕ; the neighbourhoods are the cofinite sets, closed under finite intersection ((X ∩ Y)ᶜ = Xᶜ ∪ Yᶜ).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise220.mem_powerSet {X : Set ℕ} : powerSet.mem X ↔ Xᶜ.Finite

@[simp]

theorem Domain.Neighborhood.Exercise220.powerSet_master : powerSet.master = Set.univ

theorem Domain.Neighborhood.Exercise220.powerSet_inter_mem {A B : Set ℕ} (hA : powerSet.mem A) (hB : powerSet.mem B) : powerSet.mem (A ∩ B)

Cofinite sets are closed under intersection (witness-free form).

theorem Domain.Neighborhood.Exercise220.mem_compl_singleton (n : ℕ) : powerSet.mem {n}ᶜ

The complement of a singleton is a neighbourhood (it represents the finite element {n}).

The identification |𝒫| ≃o Set ℕ.

def Domain.Neighborhood.Exercise220.toSet (x : powerSet.Element) : Set ℕ

The subset of ℕ represented by an element: n ∈ toSet x ↔ {n}ᶜ ∈ x.

Equations

• Domain.Neighborhood.Exercise220.toSet x = {n : ℕ | x.mem {n}ᶜ}

@[simp]

theorem Domain.Neighborhood.Exercise220.mem_toSet {x : powerSet.Element} {n : ℕ} : n ∈ toSet x ↔ x.mem {n}ᶜ

def Domain.Neighborhood.Exercise220.ofSet (S : Set ℕ) : powerSet.Element

The filter of a subset S ⊆ ℕ: the cofinite Z with Zᶜ ⊆ S.

Equations

• Domain.Neighborhood.Exercise220.ofSet S = { mem := fun (Z : Set ℕ) => Domain.Neighborhood.Exercise220.powerSet.mem Z ∧ Zᶜ ⊆ S, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.Exercise220.mem_compl_of_finite (x : powerSet.Element) {t : Set ℕ} (ht : t.Finite) (h : ∀ n ∈ t, x.mem {n}ᶜ) : x.mem tᶜ

Filters are determined on cofinite sets by their singleton-complements. For cofinite Z, Z ∈ x ↔ ∀ n ∈ Zᶜ, {n}ᶜ ∈ x (since Z = ⋂_{n ∈ Zᶜ} {n}ᶜ, a finite intersection).

theorem Domain.Neighborhood.Exercise220.toSet_ofSet (S : Set ℕ) : toSet (ofSet S) = S

theorem Domain.Neighborhood.Exercise220.ofSet_toSet (x : powerSet.Element) : ofSet (toSet x) = x

theorem Domain.Neighborhood.Exercise220.ofSet_mono {S S' : Set ℕ} (h : S ⊆ S') : ofSet S ≤ ofSet S'

ofSet is monotone in the set.

def Domain.Neighborhood.Exercise220.equivSetNat : powerSet.Element ≃o Set ℕ

Exercise 2.20 — the identification |𝒫| ≅ (Set ℕ, ⊆).

Equations

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

The shift maps x + 1 and x − 1.

def Domain.Neighborhood.Exercise220.succSet (S : Set ℕ) : Set ℕ

S + 1 = {n + 1 ∣ n ∈ S}.

Equations

• Domain.Neighborhood.Exercise220.succSet S = (fun (x : ℕ) => x + 1) '' S

def Domain.Neighborhood.Exercise220.predSet (S : Set ℕ) : Set ℕ

S − 1 = {n ∣ n + 1 ∈ S}.

Equations

• Domain.Neighborhood.Exercise220.predSet S = {n : ℕ | n + 1 ∈ S}

@[simp]

theorem Domain.Neighborhood.Exercise220.mem_predSet {S : Set ℕ} {n : ℕ} : n ∈ predSet S ↔ n + 1 ∈ S

theorem Domain.Neighborhood.Exercise220.succSet_mono {S T : Set ℕ} (h : S ⊆ T) : succSet S ⊆ succSet T

theorem Domain.Neighborhood.Exercise220.predSet_mono {S T : Set ℕ} (h : S ⊆ T) : predSet S ⊆ predSet T

def Domain.Neighborhood.Exercise220.succMap : ApproximableMap powerSet powerSet

Exercise 2.20 — x + 1 is approximable. X f Z ↔ Zᶜ ⊆ (Xᶜ + 1).

Equations

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

def Domain.Neighborhood.Exercise220.predMap : ApproximableMap powerSet powerSet

Exercise 2.20 — x − 1 is approximable. X f Z ↔ Zᶜ ⊆ (Xᶜ − 1).

Equations

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

theorem Domain.Neighborhood.Exercise220.toSet_succMap (x : powerSet.Element) : toSet (succMap.toElementMap x) = succSet (toSet x)

theorem Domain.Neighborhood.Exercise220.toSet_predMap (x : powerSet.Element) : toSet (predMap.toElementMap x) = predSet (toSet x)

Union and intersection as two-variable approximable maps.

def Domain.Neighborhood.Exercise220.unionMap : ApproximableMap₂ powerSet powerSet powerSet

Exercise 2.20 — x ∪ y is approximable (two variables). X, Y f Z ↔ X ∩ Y ⊆ Z ((Xᶜ ∪ Yᶜ)ᶜ = X ∩ Y).

Equations

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

def Domain.Neighborhood.Exercise220.interMap₂ : ApproximableMap₂ powerSet powerSet powerSet

Exercise 2.20 — x ∩ y is approximable (two variables). X, Y f Z ↔ X ∪ Y ⊆ Z ((Xᶜ ∩ Yᶜ)ᶜ = X ∪ Y).

Equations

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

theorem Domain.Neighborhood.Exercise220.toSet_unionMap (x y : powerSet.Element) : toSet (unionMap.toElementMap₂ x y) = toSet x ∪ toSet y

theorem Domain.Neighborhood.Exercise220.toSet_interMap₂ (x y : powerSet.Element) : toSet (interMap₂.toElementMap₂ x y) = toSet x ∩ toSet y