Exercise 1.25 (Scott 1981, PRG-19, §1) — final segments of an ordinal

Scott: let Δ be a well-ordered set (ordinal) and let 𝒟 be the family of non-empty final segments of Δ. Describe |𝒟|; are all elements finite; is every approximation to a finite element finite?

For a linear order, the final segments are exactly the non-empty upper sets (IsUpperSet). Any two upper sets of a linear order are nested (upperSet_subset_or), so the family is a neighbourhood system by Scott's nested-or-disjoint criterion (finalSegmentSystem).

Classification of |𝒟|. For a well-order every non-empty upper set is Set.Ici a with a its minimum (exists_Ici_of_mem). Hence a filter x is completely described by its trace lowerSetOf x = {a ∣ Ici a ∈ x}, which is a non-empty lower set of Δ, and x ↦ lowerSetOf x is an order isomorphism

|𝒟| ≃o {S : Set Δ ∣ S non-empty lower set} (ordered by ⊆) — finalSegmentClassify.

So |𝒟| is the lattice of non-empty initial segments of Δ (the "cuts" of Δ).

Total / finite. The greatest element is the filter of all neighbourhoods (topElement), which is the unique total element (topElement_isTotal, eq_topElement_of_isTotal). The finite elements are the principal filters ↑(Ici a). When Δ has no greatest element (e.g. ℕ = ω) the total element is not finite (topElement_not_principal_of_noMax): not all elements are finite.

The system and Ici lemmas are [propext, Quot.sound]; the classification's surjectivity uses the well-ordering (WellFounded.has_min), so it is classical.

theorem Domain.Neighborhood.FinalSegment.upperSet_subset_or {Δ : Type u_1} [LinearOrder Δ] {X Y : Set Δ} (hX : IsUpperSet X) (hY : IsUpperSet Y) : X ⊆ Y ∨ Y ⊆ X

In a linear order, any two upper sets are nested. (Hence final segments are nested-or-disjoint — in fact always nested.)

def Domain.Neighborhood.FinalSegment.finalSegmentSystem (Δ : Type u_1) [LinearOrder Δ] [Nonempty Δ] : NeighborhoodSystem Δ

Exercise 1.25 — the final-segment neighbourhood system. Over a (non-empty) linear order Δ, the non-empty upper sets (final segments) form a neighbourhood system. Built via ofNestedOrDisjoint since any two upper sets are nested (upperSet_subset_or).

Equations

• Domain.Neighborhood.FinalSegment.finalSegmentSystem Δ = Domain.Neighborhood.NeighborhoodSystem.ofNestedOrDisjoint (fun (X : Set Δ) => X.Nonempty ∧ IsUpperSet X) Set.univ ⋯ ⋯ ⋯

@[simp]

theorem Domain.Neighborhood.FinalSegment.mem_def {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] {X : Set Δ} : (finalSegmentSystem Δ).mem X ↔ X.Nonempty ∧ IsUpperSet X

@[simp]

theorem Domain.Neighborhood.FinalSegment.master_eq {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] : (finalSegmentSystem Δ).master = Set.univ

theorem Domain.Neighborhood.FinalSegment.Ici_mem {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (a : Δ) : (finalSegmentSystem Δ).mem (Set.Ici a)

Each Set.Ici a is a (non-empty, upper) neighbourhood.

theorem Domain.Neighborhood.FinalSegment.principal_Ici_le_iff {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (a b : Δ) : (finalSegmentSystem Δ).principal ⋯ ≤ (finalSegmentSystem Δ).principal ⋯ ↔ a ≤ b

The principal finite elements ↑(Ici a); the correspondence a ↦ ↑(Ici a) is order-reversing (Ici a ⊆ Ici b ↔ b ≤ a), one of Scott's "finite elements".

Well-order: every neighbourhood is Ici (its minimum).

theorem Domain.Neighborhood.FinalSegment.exists_Ici_of_mem {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] [WellFoundedLT Δ] {X : Set Δ} (hX : (finalSegmentSystem Δ).mem X) : ∃ (a : Δ), X = Set.Ici a

Well-order key lemma. In a well-order, every non-empty upper set is Set.Ici a, where a is its least element.

The classification of |𝒟| as the non-empty lower sets (initial

segments).

def Domain.Neighborhood.FinalSegment.lowerSetOf {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (x : (finalSegmentSystem Δ).Element) : Set Δ

The trace lowerSetOf x = {a ∣ Ici a ∈ x} of a filter x.

Equations

• Domain.Neighborhood.FinalSegment.lowerSetOf x = {a : Δ | x.mem (Set.Ici a)}

theorem Domain.Neighborhood.FinalSegment.lowerSetOf_nonempty {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] [WellFoundedLT Δ] (x : (finalSegmentSystem Δ).Element) : (lowerSetOf x).Nonempty

theorem Domain.Neighborhood.FinalSegment.lowerSetOf_isLowerSet {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (x : (finalSegmentSystem Δ).Element) : IsLowerSet (lowerSetOf x)

def Domain.Neighborhood.FinalSegment.ofLowerSet {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (S : Set Δ) (hSne : S.Nonempty) : (finalSegmentSystem Δ).Element

The filter built from a non-empty lower set S: the neighbourhoods that contain some Ici a with a ∈ S.

Equations

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

theorem Domain.Neighborhood.FinalSegment.lowerSetOf_ofLowerSet {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (S : Set Δ) (hSne : S.Nonempty) (hS : IsLowerSet S) : lowerSetOf (ofLowerSet S hSne) = S

theorem Domain.Neighborhood.FinalSegment.ofLowerSet_lowerSetOf {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] [WellFoundedLT Δ] (x : (finalSegmentSystem Δ).Element) : ofLowerSet (lowerSetOf x) ⋯ = x

def Domain.Neighborhood.FinalSegment.finalSegmentClassify {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] [WellFoundedLT Δ] : (finalSegmentSystem Δ).Element ≃o { S : Set Δ // S.Nonempty ∧ IsLowerSet S }

Exercise 1.25 — classification of |𝒟|. For a well-order Δ, the domain of non-empty final segments is order-isomorphic to the poset of non-empty initial segments (lower sets) of Δ under inclusion: x ↦ {a ∣ Ici a ∈ x}. (So |𝒟| is the lattice of cuts of Δ.)

Equations

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

Total elements and finiteness (Scott's prose questions).

def Domain.Neighborhood.FinalSegment.topElement {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] : (finalSegmentSystem Δ).Element

The greatest element: the filter of all neighbourhoods.

Equations

• Domain.Neighborhood.FinalSegment.topElement = { mem := fun (X : Set Δ) => (Domain.Neighborhood.FinalSegment.finalSegmentSystem Δ).mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.FinalSegment.le_topElement {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (x : (finalSegmentSystem Δ).Element) : x ≤ topElement

theorem Domain.Neighborhood.FinalSegment.topElement_isTotal {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] : (finalSegmentSystem Δ).IsTotal topElement

Exercise 1.25 — the unique total element. The filter of all neighbourhoods is total (⊑-maximal).

theorem Domain.Neighborhood.FinalSegment.eq_topElement_of_isTotal {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] {x : (finalSegmentSystem Δ).Element} (hx : (finalSegmentSystem Δ).IsTotal x) : x = topElement

It is the unique total element: any total x equals topElement.

theorem Domain.Neighborhood.FinalSegment.topElement_not_principal_of_noMax {Δ : Type u_1} [LinearOrder Δ] [Nonempty Δ] (hnomax : ∀ (a : Δ), ∃ (b : Δ), a < b) (a : Δ) : topElement ≠ (finalSegmentSystem Δ).principal ⋯

Exercise 1.25 — not all elements are finite. If Δ has no greatest element (e.g. Δ = ℕ = ω), the total element topElement is not a principal filter ↑(Ici a): pick b > a, then Ici b ∈ topElement but Ici a ⊄ Ici b. So |𝒟| has a non-finite (limit) element.