Exercise 1.24 (Scott 1981, PRG-19, §1) — every partial element extends to a

total one (AC)

Scott (for set theorists): using the Axiom of Choice, prove that in every domain a partial element can always be extended to a total element. (Hint: the union of every transfinite chain of filters is again a filter.)

This file formalizes:

• chainUnion C hne hchain — the union ⋃ C of a non-empty chain C of filters is itself a filter (V.Element); the only non-trivial axiom is inter_mem, which uses chain-directedness to find a single member of C containing both factors. Plus le_chainUnion (every member of the chain is ⊑ the union).
• exists_total_ge x — with Zorn's lemma (zorn_le_nonempty_Ici₀), every element x has a total element t above it (x ⊑ t ∧ IsTotal t). The chains in Ici x are bounded above by their chainUnion, so Zorn produces a maximal — i.e. total — element.

Whether this is equivalent to AC is left as prose (Scott's question); we do not formalize the reversal. This is the explicitly classical exercise: exists_total_ge legitimately uses Classical.choice through zorn_le_nonempty_Ici₀. The chainUnion construction is choice-free ([propext, Quot.sound]).

def Domain.Neighborhood.NeighborhoodSystem.chainUnion {α : Type u_1} (V : NeighborhoodSystem α) (C : Set V.Element) (hne : C.Nonempty) (hchain : IsChain (fun (x1 x2 : V.Element) => x1 ≤ x2) C) : V.Element

Exercise 1.24 — the union of a chain of filters is a filter. For a non-empty chain C of filters, ⋃ C = {X ∣ ∃ x ∈ C, X ∈ x} is again a filter. The intersection axiom uses chain totality: given X ∈ x and Y ∈ y with x, y ∈ C, one of x ⊑ y, y ⊑ x holds, and the larger filter contains both X and Y, hence X ∩ Y.

Equations

• V.chainUnion C hne hchain = { mem := fun (X : Set α) => ∃ x ∈ C, x.mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.le_chainUnion {α : Type u_1} (V : NeighborhoodSystem α) (C : Set V.Element) (hne : C.Nonempty) (hchain : IsChain (fun (x1 x2 : V.Element) => x1 ≤ x2) C) {x : V.Element} (hx : x ∈ C) : x ≤ V.chainUnion C hne hchain

Every member of the chain approximates the union ⋃ C.

theorem Domain.Neighborhood.NeighborhoodSystem.exists_total_ge {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : ∃ (t : V.Element), V.IsTotal t ∧ x ≤ t

Exercise 1.24 — partial elements extend to total ones (AC). Using Zorn's lemma, every element x admits a total element t with x ⊑ t. The upper bound of any non-empty chain in Ici x is its chainUnion, so a maximal element exists; maximality is exactly totality (IsMax = IsTotal).