Theorem 1.11 (Scott 1981, PRG-19, §1) — closure of |𝒟| under sequential ⋂

and ascending ⋃

If 𝒟 is a neighbourhood system and xₙ ∈ |𝒟| for n = 0, 1, 2, …, then

• (i) ⋂ₙ xₙ ∈ |𝒟|;
• (ii) ⋃ₙ xₙ ∈ |𝒟|, provided x₀ ⊆ x₁ ⊆ x₂ ⊆ ⋯ (an ascending chain).

We realize each as a concrete Element:

• iInter x has membership X ∈ ⋂ₙ xₙ iff ∀ n, X ∈ xₙ. All four filter laws are pointwise. It is the greatest lower bound (iInter_le, le_iInter): Scott's "best element that approximates all of the xₙ; exactly what is common to all".
• iUnion x hmono (with hmono : Monotone x) has X ∈ ⋃ₙ xₙ iff ∃ n, X ∈ xₙ. Only filter law (ii) (closure under ∩) needs the proviso: from X ∈ xₙ, Y ∈ xₘ take k = max n m, where monotonicity puts both X, Y ∈ x_k, so X ∩ Y ∈ x_k. It is the least upper bound (le_iUnion, iUnion_le): "just what the increasing sequence approximates".

Everything is constructive ([propext, Quot.sound]).

(i) Countable intersection.

def Domain.Neighborhood.NeighborhoodSystem.iInter {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) : V.Element

Theorem 1.11 (i). The intersection ⋂ₙ xₙ = {X ∣ ∀ n, X ∈ xₙ} of a sequence of elements is again an element of |𝒟|. (No proviso: all of 1.6(i)–(iii) are pointwise.)

Equations

• V.iInter x = { mem := fun (X : Set α) => ∀ (n : ℕ), (x n).mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_iInter {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) {X : Set α} : (V.iInter x).mem X ↔ ∀ (n : ℕ), (x n).mem X

theorem Domain.Neighborhood.NeighborhoodSystem.iInter_le {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (n : ℕ) : V.iInter x ≤ x n

⋂ₙ xₙ ⊑ xₙ: the intersection approximates every member of the sequence.

theorem Domain.Neighborhood.NeighborhoodSystem.le_iInter {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (y : V.Element) (h : ∀ (n : ℕ), y ≤ x n) : y ≤ V.iInter x

⋂ₙ xₙ is the greatest lower bound: anything approximating all xₙ approximates ⋂ₙ xₙ.

(ii) Ascending countable union.

def Domain.Neighborhood.NeighborhoodSystem.iUnion {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (hmono : Monotone x) : V.Element

Theorem 1.11 (ii). For an ascending sequence x₀ ⊑ x₁ ⊑ ⋯, the union ⋃ₙ xₙ = {X ∣ ∃ n, X ∈ xₙ} is again an element of |𝒟|. The proviso (Monotone x) is used only in the intersection law: X ∈ xₙ, Y ∈ xₘ ⟹ both in x_{max n m}.

Equations

• V.iUnion x hmono = { mem := fun (X : Set α) => ∃ (n : ℕ), (x n).mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_iUnion {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (hmono : Monotone x) {X : Set α} : (V.iUnion x hmono).mem X ↔ ∃ (n : ℕ), (x n).mem X

theorem Domain.Neighborhood.NeighborhoodSystem.le_iUnion {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (hmono : Monotone x) (n : ℕ) : x n ≤ V.iUnion x hmono

xₙ ⊑ ⋃ₙ xₙ: every member of the sequence approximates the union.

theorem Domain.Neighborhood.NeighborhoodSystem.iUnion_le {α : Type u_1} (V : NeighborhoodSystem α) (x : ℕ → V.Element) (hmono : Monotone x) (y : V.Element) (h : ∀ (n : ℕ), x n ≤ y) : V.iUnion x hmono ≤ y

⋃ₙ xₙ is the least upper bound: anything approximated by all xₙ approximates the union from above.