March 1972 correction (Scott, pp. 135–136)

Robin Milner observed that Scott's remark before Proposition 2.5 was wrong: a T₀-topology on a complete lattice need not have every open set Scott-open. The two extreme T₀-topologies inducing the same partial order are generated by

• {x | not x <= y} (the lower subbasic sets), and
• {x | y ⊑ x} (principal up-sets).

The corrected proofs of Propositions 2.9, 2.10, and 3.3 assume the given topology is contained in the Scott (lattice) topology: every open set of the given topology is Scott-open.

For Proposition 2.10, Scott distinguishes ambient joins in D' from subspace joins in a retract D ⊆ D': the prime in ⊔S′ marks the index (join taken in D'), not a "primed join" operator. The retraction identity used in the corrected argument is j(⊔S′) = ⊔S for directed S ⊆ D (see IsContinuousLatticeRetraction.retr_ambientSSup_eq_sSup in FunctionSpaces.lean).

Page 136 adds that function spaces pose no subspace/sup mismatch: lubs are computed pointwise, so the product (relativized) topology is contained in the Scott topology once the Milner hypothesis is in place.

Extreme T₀-topologies inducing the order

def Domain.ContinuousLattice.scottLowerSubbasisSet {D : Type u_1} [CompleteLattice D] (y : D) : Set D

Lower subbasic set {x | not x <= y} from Scott's March 1972 correction.

Equations

• Domain.ContinuousLattice.scottLowerSubbasisSet y = {x : D | ¬x ≤ y}

def Domain.ContinuousLattice.scottPrincipalUpSet {D : Type u_1} [CompleteLattice D] (y : D) : Set D

Upper subbasic set {x | y ⊑ x} (principal up-set) from the correction.

Equations

• Domain.ContinuousLattice.scottPrincipalUpSet y = Set.Ici y

Milner hypothesis for 2.9, 2.10, 3.3

def Domain.ContinuousLattice.CoarserThanScottTopology {D : Type u_1} [CompleteLattice D] (τ : TopologicalSpace D) : Prop

March 1972 correction. The given topology τ is coarser than (or equal to) the Scott topology: every set open in τ is Scott-open. Equivalently Opens(τ) ⊆ Opens(Scott), i.e. scottTopologicalSpace ≤ τ in mathlib's order on topologies.

Equations

• Domain.ContinuousLattice.CoarserThanScottTopology τ = (Domain.ContinuousLattice.scottTopologicalSpace ≤ τ)

theorem Domain.ContinuousLattice.scottOpen_of_coarserThanScott {D : Type u_1} [CompleteLattice D] {τ : TopologicalSpace D} (hτ : CoarserThanScottTopology τ) {U : Set D} (hU : IsOpen U) : ScottOpen U