Exercise 1.27 (Scott 1981, PRG-19, §1) — bounded sets and least upper bounds

Scott introduces bounded sets of elements as the analogue, for |𝒟|, of consistent sequences of neighbourhoods. A set X ⊆ |𝒟| is bounded iff it has an upper bound y ∈ |𝒟| (x ⊑ y for all x ∈ X), and then

⊔X = ⋂ {y ∣ x ⊑ y for all x ∈ X}

is its least upper bound. This file formalizes:

• Bounded X and sSup X hX := sInf (upper bounds of X) — the upper-bound family is non-empty exactly because X is bounded, so we reuse sInf from Exercise 1.18; the lub laws le_sSup / sSup_le are then immediate from le_sInf / sInf_le;
• consistent_pair_iff_bounded — for U, W ∈ 𝒟, the pair ⟨U, W⟩ is Consistent iff {↑U, ↑W} is bounded ("boundedness is for elements what consistency is for neighbourhoods");
• bounded_iff_finite_bounded — with the aid of Exercise 1.18, X is bounded iff every finite subset of X is bounded; the hard direction builds the bound as the leastFilter of C = ⋃_{x∈X} x, whose finite consistency comes from the finite bounds.

The constructions (sSup) are [propext, Quot.sound]. The hard direction of bounded_iff_finite_bounded selects a finite witness set via Classical.choice; this is a proof, so the construction stays choice-free.

def Domain.Neighborhood.NeighborhoodSystem.Bounded {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) : Prop

Exercise 1.27 — bounded set of elements. X ⊆ |𝒟| is bounded iff it has an upper bound y ∈ |𝒟|: x ⊑ y for all x ∈ X.

Equations

• V.Bounded X = ∃ (y : V.Element), ∀ x ∈ X, x ≤ y

def Domain.Neighborhood.NeighborhoodSystem.upperBounds {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) : Set V.Element

The family of upper bounds of X: {y ∣ x ⊑ y for all x ∈ X}.

Equations

• V.upperBounds X = {y : V.Element | ∀ x ∈ X, x ≤ y}

theorem Domain.Neighborhood.NeighborhoodSystem.upperBounds_nonempty {α : Type u_1} (V : NeighborhoodSystem α) {X : Set V.Element} (hX : V.Bounded X) : (V.upperBounds X).Nonempty

If X is bounded then its upper-bound family is non-empty (it contains the witness).

def Domain.Neighborhood.NeighborhoodSystem.sSup {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) (hX : V.Bounded X) : V.Element

Exercise 1.27 — ⊔X. The least upper bound of a bounded X, defined à la Scott as the intersection of all upper bounds: ⊔X = ⋂ {y ∣ x ⊑ y all x∈X}. Reusing sInf from Exercise 1.18 on the (non-empty, because bounded) family of upper bounds.

Equations

• V.sSup X hX = V.sInf (V.upperBounds X) ⋯

theorem Domain.Neighborhood.NeighborhoodSystem.le_sSup {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) (hX : V.Bounded X) {x : V.Element} (hx : x ∈ X) : x ≤ V.sSup X hX

Exercise 1.27 — ⊔X is an upper bound. Each x ∈ X satisfies x ⊑ ⊔X.

theorem Domain.Neighborhood.NeighborhoodSystem.sSup_le {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) (hX : V.Bounded X) {z : V.Element} (hz : ∀ x ∈ X, x ≤ z) : V.sSup X hX ≤ z

Exercise 1.27 — ⊔X is least. Any upper bound z of X satisfies ⊔X ⊑ z.

Boundedness of {↑U, ↑W} iff consistency of ⟨U, W⟩.

def Domain.Neighborhood.NeighborhoodSystem.pairSeq {α : Type u_1} (U W : Set α) : ℕ → Set α

The two-term sequence ⟨U, W⟩ as a function ℕ → Set α (used to phrase Consistent).

Equations

• Domain.Neighborhood.NeighborhoodSystem.pairSeq U W i = if i = 0 then U else W

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_pairSeq {α : Type u_1} (V : NeighborhoodSystem α) (U W : Set α) : V.interUpTo (pairSeq U W) 2 = V.master ∩ U ∩ W

theorem Domain.Neighborhood.NeighborhoodSystem.consistent_pair_iff_bounded {α : Type u_1} (V : NeighborhoodSystem α) {U W : Set α} (hU : V.mem U) (hW : V.mem W) : V.Consistent (pairSeq U W) 2 ↔ V.Bounded {V.principal hU, V.principal hW}

Exercise 1.27 — "boundedness is for elements what consistency is for neighbourhoods". For U, W ∈ 𝒟, the pair ⟨U, W⟩ is consistent in 𝒟 iff {↑U, ↑W} is bounded in |𝒟|.

→ packages the consistency witness Z into the principal filter ↑Z, which lies above both ↑U and ↑W (via principal_le_iff). ← uses that any bound y contains both U and W, hence U ∩ W ∈ y ⊆ 𝒟, giving U ∩ W as the consistency witness.

Boundedness is finitary (with the aid of Exercise 1.18).

theorem Domain.Neighborhood.NeighborhoodSystem.bounded_iff_finite_bounded {α : Type u_1} (V : NeighborhoodSystem α) (X : Set V.Element) : V.Bounded X ↔ ∀ S ⊆ X, S.Finite → V.Bounded S

Exercise 1.27 — boundedness is finitary. X ⊆ |𝒟| is bounded iff every finite subset of X is bounded. The forward direction reuses any global bound. The reverse direction is the content: assemble C = ⋃_{x∈X} x (the neighbourhoods of all members of X); C is finitely consistent because any finite sequence drawn from C comes from finitely many members of X, which form a finite subset, hence bounded — that bound's filter contains the whole finite sequence, so its intersection lies in 𝒟. The least filter leastFilter C (Exercise 1.18) is then an upper bound of X.