Exercise 1.12 (Scott 1981, PRG-19, §1) — the final-segment system on ℕ

Let Δ = ℕ and take as neighbourhoods the final segments (tails)

tail n = {m ∈ ℕ ∣ n ≤ m},

so tail 0 = ℕ = Δ and tail 0 ⊇ tail 1 ⊇ tail 2 ⊇ ⋯ is a descending chain (Scott's {m ∣ m > n} is tail (n+1)). This generalizes Example 1.3 (a chain) to the countably infinite case.

Deliverables:

• neighborhoodSystem : NeighborhoodSystem ℕ (the tails are pairwise nested, so Factoid 1.4a applies) — verifies it is a neighbourhood system.
• Finite elements. fin n = ↑(tail n), the principal filters; they form an ascending ω-chain fin 0 ⊏ fin 1 ⊏ ⋯ (fin_le_iff, fin_strictMono).
• The limit / total element. top = 𝒟 itself (all tails) is the greatest element (le_top), is the unique total (maximal) element (top_isTotal, isTotal_iff_top).
• Classification (the "only one limit element" hint): every element is either a finite fin n or the limit top (element_eq). This single result is classical (it decides whether the set of indices in x is bounded — Nat.find over a ¬-predicate); everything else is constructive.

def Domain.Neighborhood.Exercise112.tail (n : ℕ) : Set ℕ

The final segment (tail) tail n = {m ∣ n ≤ m}; the neighbourhood "all integers ≥ n".

Equations

• Domain.Neighborhood.Exercise112.tail n = {m : ℕ | n ≤ m}

@[simp]

theorem Domain.Neighborhood.Exercise112.mem_tail {n m : ℕ} : m ∈ tail n ↔ n ≤ m

theorem Domain.Neighborhood.Exercise112.tail_subset_iff {n m : ℕ} : tail n ⊆ tail m ↔ m ≤ n

A longer tail is a smaller set: tail n ⊆ tail m ↔ m ≤ n.

theorem Domain.Neighborhood.Exercise112.tail_inter (n m : ℕ) : tail n ∩ tail m = tail (max n m)

tail n ∩ tail m = tail (max n m) (the intersection of two tails is the shorter one).

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

Membership in the final-segment system: X is a neighbourhood iff X = tail n for some n.

Equations

• Domain.Neighborhood.Exercise112.mem X = ∃ (n : ℕ), X = Domain.Neighborhood.Exercise112.tail n

theorem Domain.Neighborhood.Exercise112.nestedOrDisjoint : NestedOrDisjoint mem

def Domain.Neighborhood.Exercise112.neighborhoodSystem : NeighborhoodSystem ℕ

Exercise 1.12. The final-segment neighbourhood system on ℕ (master Δ = tail 0 = ℕ).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise112.ns_mem {X : Set ℕ} : neighborhoodSystem.mem X ↔ ∃ (n : ℕ), X = tail n

theorem Domain.Neighborhood.Exercise112.mem_tail_nbhd (n : ℕ) : neighborhoodSystem.mem (tail n)

Finite elements: the principal filters fin n = ↑(tail n).

def Domain.Neighborhood.Exercise112.fin (n : ℕ) : neighborhoodSystem.Element

The finite element fin n = ↑(tail n) (principal filter of the tail).

Equations

• Domain.Neighborhood.Exercise112.fin n = Domain.Neighborhood.Exercise112.neighborhoodSystem.principal ⋯

theorem Domain.Neighborhood.Exercise112.fin_le_iff (n m : ℕ) : fin n ≤ fin m ↔ n ≤ m

The finite elements form an ascending chain: fin n ⊑ fin m ↔ n ≤ m.

theorem Domain.Neighborhood.Exercise112.fin_strictMono : StrictMono fin

The chain fin 0 ⊏ fin 1 ⊏ ⋯ is strictly increasing.

The limit element: the whole system 𝒟, the greatest / unique total

element.

def Domain.Neighborhood.Exercise112.top : neighborhoodSystem.Element

The limit element top: the filter of all tails (Scott's single limit node).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise112.mem_top {X : Set ℕ} : top.mem X ↔ neighborhoodSystem.mem X

theorem Domain.Neighborhood.Exercise112.le_top (x : neighborhoodSystem.Element) : x ≤ top

top is the greatest element of |𝒟|: every element approximates it.

theorem Domain.Neighborhood.Exercise112.top_isTotal : neighborhoodSystem.IsTotal top

top is a total (maximal) element.

theorem Domain.Neighborhood.Exercise112.isTotal_iff_top (x : neighborhoodSystem.Element) : neighborhoodSystem.IsTotal x ↔ x = top

top is the unique total element: an element is total iff it equals top.

Classification: finite fin n, or the limit top (classical).

theorem Domain.Neighborhood.Exercise112.element_eq (x : neighborhoodSystem.Element) : (∃ (n : ℕ), x = fin n) ∨ x = top

Exercise 1.12 (classification). Every element is either a finite element fin n or the single limit element top. Classical: it decides whether the indices present in x are bounded. (Hint realized: "there is only one limit element.")