Solovay's complete Boolean algebra construction

This file formalizes the construction in Robert M. Solovay's New Proof of a Theorem of Gaifman and Hales. It realizes the resulting complete Boolean algebra as the clopen algebra of its Stone space and develops the analytic facts needed for the Gao--Leung counterexample.

@[reducible, inline]

abbrev OrderClosures.RegularOpen (X : Type u) [TopologicalSpace X] : Type u

The regular-open completion of the open-set Boolean algebra, used as the complete Boolean algebra in Solovay's construction.

Equations

• OrderClosures.RegularOpen X = Heyting.Regular (TopologicalSpace.Opens X)

@[instance_reducible]

noncomputable instance OrderClosures.regularOpenCompleteLattice (X : Type u) [TopologicalSpace X] : CompleteLattice (RegularOpen X)

Supplies arbitrary suprema and infima on regular open sets; required for complete-generation arguments below.

Equations

• OrderClosures.regularOpenCompleteLattice X = Heyting.Regular.gi.liftCompleteLattice

@[instance_reducible]

noncomputable instance OrderClosures.regularOpenCompleteBooleanAlgebra (X : Type u) [TopologicalSpace X] : CompleteBooleanAlgebra (RegularOpen X)

Bundles the complete Boolean-algebra structure of regular open sets; used as the algebra whose Stone spectrum forms the counterexample.

Equations

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

def OrderClosures.regularOpenOfClopen {X : Type u} [TopologicalSpace X] (s : Set X) (hs : IsClopen s) : RegularOpen X

Regards a clopen set as a regular open element; used to turn finite cylinders into Boolean-algebra generators.

Equations

• OrderClosures.regularOpenOfClopen s hs = ⟨{ carrier := s, is_open' := ⋯ }, ⋯⟩

@[simp]

theorem OrderClosures.coe_regularOpenOfClopen {X : Type u} [TopologicalSpace X] (s : Set X) (hs : IsClopen s) : ↑↑(regularOpenOfClopen s hs) = s

theorem OrderClosures.regularOpen_ext {X : Type u} [TopologicalSpace X] {U V : RegularOpen X} (h : ↑↑U = ↑↑V) : U = V

Reduces equality of regular open sets to equality of carriers; used to simplify Boolean-algebra computations in the Solovay construction.

theorem OrderClosures.regularOpenOfClopen_congr {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) (h : s = t) : regularOpenOfClopen s hs = regularOpenOfClopen t ht

Makes the regular-open constructor respect equality of clopen carriers; used when rewriting cylinder identities.

theorem OrderClosures.regularOpenOfClopen_inf {X : Type u} [TopologicalSpace X] (s t : Set X) (hs : IsClopen s) (ht : IsClopen t) : regularOpenOfClopen (s ∩ t) ⋯ = regularOpenOfClopen s hs ⊓ regularOpenOfClopen t ht

Computes intersections of clopen sets inside the regular-open algebra; used for finite cylinder meets and Boolean subalgebras.

theorem OrderClosures.regularOpenOfClopen_compl {X : Type u} [TopologicalSpace X] (s : Set X) (hs : IsClopen s) : regularOpenOfClopen sᶜ ⋯ = (regularOpenOfClopen s hs)ᶜ

Computes complements of clopen sets inside the regular-open algebra; used to show the cylinder-generated family is a Boolean subalgebra.

theorem OrderClosures.regularOpenOfClopen_eq_sSup {X : Type u} [TopologicalSpace X] (S : Set (RegularOpen X)) (t : Set X) (ht : IsClopen t) (hunion : t = ⋃ U ∈ S, ↑↑U) : regularOpenOfClopen t ht = sSup S

Expresses a clopen union as a supremum of regular-open elements; used to derive the explicit Solovay generator formulas.

theorem OrderClosures.regularOpen_eq_sSup_of_union {X : Type u} [TopologicalSpace X] (U : RegularOpen X) (S : Set (RegularOpen X)) (hunion : ↑↑U = ⋃ V ∈ S, ↑↑V) : U = sSup S

Recovers a regular open set as the supremum of a family whose union is dense in it; used in the proof that the Solovay generators are complete.

@[reducible, inline]

abbrev OrderClosures.SolovayProduct (Gamma : Type u) : Type u

The countable product of the well-ordered index type on which the Solovay cylinder algebra is constructed.

Equations

• OrderClosures.SolovayProduct Gamma = (ℕ → Gamma)

def OrderClosures.solovayA (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

The basic Solovay generator comparing coordinate n with eta; these generators will completely generate the regular-open algebra.

Equations

• OrderClosures.solovayA Gamma n eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f n = eta} ⋯

def OrderClosures.solovayCylinderSet (Gamma : Type u) (F : Finset ℕ) (g : SolovayProduct Gamma) : Set (SolovayProduct Gamma)

The finite-coordinate cylinder through g; used as the topological basis recovered from the Solovay generators.

Equations

• OrderClosures.solovayCylinderSet Gamma F g = ⋂ i ∈ F, {f : OrderClosures.SolovayProduct Gamma | f i = g i}

theorem OrderClosures.isClopen_solovayCylinderSet (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (F : Finset ℕ) (g : SolovayProduct Gamma) : IsClopen (solovayCylinderSet Gamma F g)

Shows that every finite-coordinate Solovay cylinder is clopen; this allows it to define an element of the regular-open Boolean algebra.

def OrderClosures.solovayCylinder (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (F : Finset ℕ) (g : SolovayProduct Gamma) : RegularOpen (SolovayProduct Gamma)

The regular-open element associated with a finite cylinder; used to prove complete generation of every regular open set.

Equations

• OrderClosures.solovayCylinder Gamma F g = OrderClosures.regularOpenOfClopen (OrderClosures.solovayCylinderSet Gamma F g) ⋯

@[simp]

theorem OrderClosures.mem_solovayCylinderSet (Gamma : Type u) (F : Finset ℕ) (g f : SolovayProduct Gamma) : f ∈ solovayCylinderSet Gamma F g ↔ ∀ i ∈ F, f i = g i

def OrderClosures.solovayB (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) : RegularOpen (SolovayProduct Gamma)

Auxiliary coordinate-comparison element used to recover finite cylinders from the basic solovayA generators.

Equations

• OrderClosures.solovayB Gamma m n = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f m ≤ f n} ⋯

def OrderClosures.solovayLT (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

The regular-open event that coordinate n is strictly below eta; used in the Boolean identities for the generators.

Equations

• OrderClosures.solovayLT Gamma n eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f n < eta} ⋯

def OrderClosures.solovayLE (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

The regular-open event that coordinate n is at most eta; used in the well-founded recovery of exact coordinate values.

Equations

• OrderClosures.solovayLE Gamma n eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f n ≤ eta} ⋯

def OrderClosures.solovayC (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

Auxiliary comparison element combining two coordinates and a threshold; used in the recursive cylinder-generation identities.

Equations

• OrderClosures.solovayC Gamma m n eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f m < f n → f m < eta} ⋯

def OrderClosures.solovayStrict (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) : RegularOpen (SolovayProduct Gamma)

The strict comparison event between two coordinates; isolated for reuse in the formulas for solovayC and solovayBad.

Equations

• OrderClosures.solovayStrict Gamma m n = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f m < f n} ⋯

def OrderClosures.solovayNotLT (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

The complement of a strict coordinate bound; used in exact-coordinate cylinder formulas.

Equations

• OrderClosures.solovayNotLT Gamma m eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | ¬f m < eta} ⋯

def OrderClosures.solovayBad (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) (eta : Gamma) : RegularOpen (SolovayProduct Gamma)

The exceptional part of a coordinate comparison; separated so it can be eliminated in the well-founded generator induction.

Equations

• OrderClosures.solovayBad Gamma m n eta = OrderClosures.regularOpenOfClopen {f : OrderClosures.SolovayProduct Gamma | f m < f n ∧ ¬f m < eta} ⋯

def OrderClosures.IsCompleteBooleanSubalgebra {B : Type u} [CompleteBooleanAlgebra B] (L : BooleanSubalgebra B) : Prop

Closure predicate for a Boolean subalgebra under arbitrary suprema; used to formulate complete generation by the Solovay family.

Equations

• OrderClosures.IsCompleteBooleanSubalgebra L = ∀ S ⊆ ↑L, sSup S ∈ L

theorem OrderClosures.IsCompleteBooleanSubalgebra.sInf_mem {B : Type u} [CompleteBooleanAlgebra B] {L : BooleanSubalgebra B} (hL : IsCompleteBooleanSubalgebra L) (S : Set B) (hSL : S ⊆ ↑L) : sInf S ∈ L

Derives closure under arbitrary infima from closure under arbitrary suprema and complement; used repeatedly for the generated Boolean algebra.

theorem OrderClosures.solovayLT_eq_sSup (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : solovayLT Gamma n eta = sSup (solovayA Gamma n '' Set.Iio eta)

Expresses the strict-order event as a supremum of basic generators; used to place it in every complete subalgebra containing solovayA.

theorem OrderClosures.solovayStrict_eq (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) : solovayStrict Gamma m n = (solovayB Gamma n m)ᶜ

Computes the event that one coordinate is strictly below another; used in the recursive recovery of finite cylinders.

theorem OrderClosures.solovayNotLT_eq (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m : ℕ) (eta : Gamma) : solovayNotLT Gamma m eta = (solovayLT Gamma m eta)ᶜ

Computes the complementary order event; used to build exact coordinate conditions from the Solovay generators.

theorem OrderClosures.solovayBad_eq (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) (eta : Gamma) : solovayBad Gamma m n eta = solovayStrict Gamma m n ⊓ solovayNotLT Gamma m eta

Decomposes the exceptional comparison event into previously generated pieces; used in the induction recovering cylinder elements.

theorem OrderClosures.solovayC_eq (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (m n : ℕ) (eta : Gamma) : solovayC Gamma m n eta = (solovayBad Gamma m n eta)ᶜ

Gives the Boolean formula for the auxiliary comparison element solovayC; used to derive the non-strict order event.

theorem OrderClosures.solovayLE_eq_sInf (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : solovayLE Gamma n eta = sInf (Set.range fun (m : ℕ) => solovayC Gamma m n eta)

Expresses a non-strict coordinate bound as an infimum of comparison elements; used in the well-founded generator induction.

theorem OrderClosures.solovayA_eq (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) (eta : Gamma) : solovayA Gamma n eta = solovayLE Gamma n eta ⊓ (solovayLT Gamma n eta)ᶜ

Gives the fundamental Boolean identity for a Solovay generator; used to recover exact coordinate cylinders.

theorem OrderClosures.solovayA_mem_of_generators (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] [WellFoundedLT Gamma] (L : BooleanSubalgebra (RegularOpen (SolovayProduct Gamma))) (hcomplete : IsCompleteBooleanSubalgebra L) (hB : ∀ (m n : ℕ), solovayB Gamma m n ∈ L) (eta : Gamma) (n : ℕ) : solovayA Gamma n eta ∈ L

Performs the well-founded step placing all solovayA elements in a complete subalgebra generated by the basic family.

theorem OrderClosures.solovayCylinder_insert (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (i : ℕ) (F : Finset ℕ) (g : SolovayProduct Gamma) : solovayCylinder Gamma (insert i F) g = solovayA Gamma i (g i) ⊓ solovayCylinder Gamma F g

Splits a finite cylinder after inserting one coordinate; used for the induction showing all finite cylinders are generated.

theorem OrderClosures.solovayCylinder_mem (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (L : BooleanSubalgebra (RegularOpen (SolovayProduct Gamma))) (hA : ∀ (n : ℕ) (eta : Gamma), solovayA Gamma n eta ∈ L) (F : Finset ℕ) (g : SolovayProduct Gamma) : solovayCylinder Gamma F g ∈ L

Places every finite Solovay cylinder in a complete subalgebra containing the generators; used to recover arbitrary regular open sets.

def OrderClosures.solovayCylindersBelow (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (U : RegularOpen (SolovayProduct Gamma)) : Set (RegularOpen (SolovayProduct Gamma))

The basic cylinders lying below a regular open element; their supremum is used to reconstruct that element.

Equations

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

theorem OrderClosures.solovay_union_cylinders_below (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (U : RegularOpen (SolovayProduct Gamma)) : ↑↑U = ⋃ V ∈ solovayCylindersBelow Gamma U, ↑↑V

Represents the points of a regular open set by cylinders lying below it; used to express that set as a supremum of generated cylinder elements.

theorem OrderClosures.solovay_every_regularOpen_mem (Gamma : Type u) [TopologicalSpace Gamma] [DiscreteTopology Gamma] (L : BooleanSubalgebra (RegularOpen (SolovayProduct Gamma))) (hcomplete : IsCompleteBooleanSubalgebra L) (hA : ∀ (n : ℕ) (eta : Gamma), solovayA Gamma n eta ∈ L) (U : RegularOpen (SolovayProduct Gamma)) : U ∈ L

Shows every regular open element belongs to any complete subalgebra containing the Solovay generators; this proves generation of the full algebra.

theorem OrderClosures.solovay_generates_regularOpen (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] [WellFoundedLT Gamma] (L : BooleanSubalgebra (RegularOpen (SolovayProduct Gamma))) (hcomplete : IsCompleteBooleanSubalgebra L) (hB : ∀ (m n : ℕ), solovayB Gamma m n ∈ L) : L = ⊤

Packages the preceding membership argument as complete generation of the regular-open Boolean algebra; used in the Gao counterexample.

theorem OrderClosures.solovayA_injective (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (n : ℕ) : Function.Injective (solovayA Gamma n)

Shows one coordinate layer of Solovay generators is injectively indexed; used for the density-character lower bound.

def OrderClosures.IsBooleanStonePoint (B : Type u) [BooleanAlgebra B] (f : B → Bool) : Prop

The bounded-lattice equations defining a two-valued Stone point; used to realize the Stone spectrum as a closed Cantor-cube subspace.

Equations

• OrderClosures.IsBooleanStonePoint B f = (f ⊥ = ⊥ ∧ f ⊤ = ⊤ ∧ (∀ (a b : B), f (a ⊓ b) = min (f a) (f b)) ∧ ∀ (a b : B), f (a ⊔ b) = max (f a) (f b))

@[reducible, inline]

abbrev OrderClosures.BooleanStone (B : Type u) [BooleanAlgebra B] : Type u

The Stone spectrum of a Boolean algebra, represented by its two-valued bounded-lattice homomorphisms.

Equations

• OrderClosures.BooleanStone B = { f : B → Bool // OrderClosures.IsBooleanStonePoint B f }

theorem OrderClosures.isClosed_isBooleanStonePoint (B : Type u) [BooleanAlgebra B] : IsClosed {f : B → Bool | IsBooleanStonePoint B f}

Proves that the Boolean-homomorphism equations define a closed subset of the Cantor cube; used to obtain compactness of the Stone spectrum.

instance OrderClosures.booleanStoneCompactSpace (B : Type u) [BooleanAlgebra B] : CompactSpace (BooleanStone B)

Compactness inherited from the closed realization inside the Cantor cube; used throughout the continuous-function construction.

instance OrderClosures.booleanStoneT2Space (B : Type u) [BooleanAlgebra B] : T2Space (BooleanStone B)

The Stone spectrum is Hausdorff as a subspace of a product of discrete two-point spaces.

def OrderClosures.booleanStoneClopen (B : Type u) [BooleanAlgebra B] (b : B) : Set (BooleanStone B)

The clopen set of Stone points evaluating a Boolean element to true; used for the faithful Stone representation.

Equations

• OrderClosures.booleanStoneClopen B b = {x : OrderClosures.BooleanStone B | ↑x b = true}

theorem OrderClosures.isClopen_booleanStoneClopen (B : Type u) [BooleanAlgebra B] (b : B) : IsClopen (booleanStoneClopen B b)

Shows that evaluation at a Boolean element defines a clopen subset of the Stone spectrum; used for the clopen representation and its indicators.

def OrderClosures.booleanStoneHom (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) : BoundedLatticeHom B Bool

Bundles a Stone point as a bounded-lattice homomorphism; used to access its algebraic laws uniformly.

Equations

• OrderClosures.booleanStoneHom B x = { toFun := ↑x, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

theorem OrderClosures.booleanStone_apply_bot (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) : ↑x ⊥ = false

@[simp]

theorem OrderClosures.booleanStone_apply_top (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) : ↑x ⊤ = true

@[simp]

theorem OrderClosures.booleanStone_apply_inf (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) (a b : B) : ↑x (a ⊓ b) = min (↑x a) (↑x b)

@[simp]

theorem OrderClosures.booleanStone_apply_sup (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) (a b : B) : ↑x (a ⊔ b) = max (↑x a) (↑x b)

@[simp]

theorem OrderClosures.booleanStone_apply_compl (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) (a : B) : ↑x aᶜ = (↑x a)ᶜ

noncomputable def OrderClosures.booleanStonePointOfPrime (B : Type u) [BooleanAlgebra B] (J : Order.Ideal B) (hJ : J.IsPrime) : BooleanStone B

Constructs the Stone point associated with a prime ideal; used to separate Boolean elements when an order relation fails.

Equations

• OrderClosures.booleanStonePointOfPrime B J hJ = ⟨fun (b : B) => decide (b ∉ J), ⋯⟩

theorem OrderClosures.exists_booleanStonePoint_of_not_le (B : Type u) [BooleanAlgebra B] {a b : B} (hab : ¬a ≤ b) : ∃ (x : BooleanStone B), ↑x a = true ∧ ↑x b = false

Separates a failed Boolean inequality by a Stone point; used to prove faithfulness of the clopen representation.

theorem OrderClosures.booleanStoneClopen_subset_iff (B : Type u) [BooleanAlgebra B] {a b : B} : booleanStoneClopen B a ⊆ booleanStoneClopen B b ↔ a ≤ b

Identifies Boolean order with inclusion of the corresponding Stone clopens; used for injectivity and order computations.

theorem OrderClosures.booleanStoneClopen_injective (B : Type u) [BooleanAlgebra B] : Function.Injective (booleanStoneClopen B)

Proves injectivity of the Stone clopen representation; used to embed the complete Boolean algebra into continuous functions.

@[simp]

theorem OrderClosures.booleanStoneClopen_top (B : Type u) [BooleanAlgebra B] : booleanStoneClopen B ⊤ = Set.univ

@[simp]

theorem OrderClosures.booleanStoneClopen_inf (B : Type u) [BooleanAlgebra B] (a b : B) : booleanStoneClopen B (a ⊓ b) = booleanStoneClopen B a ∩ booleanStoneClopen B b

@[simp]

theorem OrderClosures.booleanStoneClopen_compl (B : Type u) [BooleanAlgebra B] (a : B) : booleanStoneClopen B aᶜ = (booleanStoneClopen B a)ᶜ

def OrderClosures.booleanStoneSignedCoordinate (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) (b : B) : B

Selects b or its complement according to a Stone coordinate; used to encode signed finite cylinders as Boolean elements.

Equations

• OrderClosures.booleanStoneSignedCoordinate B x b = if ↑x b = true then b else bᶜ

theorem OrderClosures.booleanStoneClopen_signedCoordinate (B : Type u) [BooleanAlgebra B] (x : BooleanStone B) (b : B) : booleanStoneClopen B (booleanStoneSignedCoordinate B x b) = {y : BooleanStone B | ↑y b = ↑x b}

Evaluates membership in a signed-coordinate cylinder through its Boolean element; used to translate finite Cantor cylinders to Stone clopens.

def OrderClosures.booleanStoneCylinderElement (B : Type u) [BooleanAlgebra B] (F : Finset B) (x : BooleanStone B) : B

The finite meet encoding the Cantor cylinder through a Stone point; used to produce represented clopen neighborhood bases.

Equations

• OrderClosures.booleanStoneCylinderElement B F x = F.inf (OrderClosures.booleanStoneSignedCoordinate B x)

theorem OrderClosures.booleanStoneClopen_cylinderElement (B : Type u) [BooleanAlgebra B] (F : Finset B) (x : BooleanStone B) : booleanStoneClopen B (booleanStoneCylinderElement B F x) = {y : BooleanStone B | ∀ b ∈ F, ↑y b = ↑x b}

Identifies a finite Stone-space cylinder with the clopen represented by its Boolean cylinder element; used to prove the clopen basis theorem.

theorem OrderClosures.booleanStone_clopen_basis (B : Type u) [BooleanAlgebra B] {U : Set (BooleanStone B)} (hU : IsOpen U) {x : BooleanStone B} (hxU : x ∈ U) : ∃ (b : B), x ∈ booleanStoneClopen B b ∧ booleanStoneClopen B b ⊆ U

Refines every neighborhood of a Stone point to a represented clopen; used in extremal disconnectedness and point-separation arguments.

instance OrderClosures.booleanStoneExtremallyDisconnected (B : Type u) [CompleteBooleanAlgebra B] : ExtremallyDisconnected (BooleanStone B)

Supplies extremal disconnectedness from completeness of the Boolean algebra; needed for continuous suprema in C(BooleanStone B, ℝ).

def OrderClosures.continuousFamilyLevelOpen (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) (q : ℚ) : Set K

The union of strict rational upper-level sets of a function family; used as the raw level set for the continuous supremum.

Equations

• OrderClosures.continuousFamilyLevelOpen K A q = ⋃ f ∈ A, ⇑f ⁻¹' Set.Ioi ↑q

theorem OrderClosures.isOpen_continuousFamilyLevelOpen (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) (q : ℚ) : IsOpen (continuousFamilyLevelOpen K A q)

Shows that a rational strict upper-level set of a continuous family is open; used to regularize level sets in the supremum construction.

def OrderClosures.continuousFamilyRegularizedLevel (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) (q : ℚ) : Set K

The closure of a family level set, made clopen by extremal disconnectedness; used to define pointwise rational cuts.

Equations

• OrderClosures.continuousFamilyRegularizedLevel K A q = closure (OrderClosures.continuousFamilyLevelOpen K A q)

theorem OrderClosures.isClopen_continuousFamilyRegularizedLevel (K : Type u) [TopologicalSpace K] [ExtremallyDisconnected K] (A : Set C(K, ℝ)) (q : ℚ) : IsClopen (continuousFamilyRegularizedLevel K A q)

Uses extremal disconnectedness to make regularized family level sets clopen; needed to assemble a continuous supremum.

def OrderClosures.continuousFamilyCutValues (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) (x : K) : Set ℝ

Rational thresholds whose regularized level contains x; their supremum defines the candidate least upper bound.

Equations

• OrderClosures.continuousFamilyCutValues K A x = (fun (q : ℚ) => ↑q) '' {q : ℚ | x ∈ OrderClosures.continuousFamilyRegularizedLevel K A q}

noncomputable def OrderClosures.continuousFamilySupValue (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) (x : K) : ℝ

The real supremum of the rational cut values at a point; later shown continuous and bundled as continuousFamilySup.

Equations

• OrderClosures.continuousFamilySupValue K A x = sSup (OrderClosures.continuousFamilyCutValues K A x)

theorem OrderClosures.continuousFamilyRegularizedLevel_antitone (K : Type u) [TopologicalSpace K] (A : Set C(K, ℝ)) : Antitone (continuousFamilyRegularizedLevel K A)

Shows that regularized upper-level sets decrease with the threshold; used to prove consistency of the cut-value construction.

theorem OrderClosures.continuousFamilyCutValues_nonempty (K : Type u) [TopologicalSpace K] {A : Set C(K, ℝ)} (hA : A.Nonempty) (x : K) : (continuousFamilyCutValues K A x).Nonempty

Supplies rational cut values at each point for a nonempty family; needed to define the pointwise cut supremum.

theorem OrderClosures.continuousFamilyCutValues_bddAbove (K : Type u) [TopologicalSpace K] {A : Set C(K, ℝ)} {h : C(K, ℝ)} (hh : h ∈ upperBounds A) (x : K) : BddAbove (continuousFamilyCutValues K A x)

Bounds the rational cut values using a common upper bound of the family; used to make their real supremum well-defined.

theorem OrderClosures.continuousFamilyCutValue_le_upperBound (K : Type u) [TopologicalSpace K] {A : Set C(K, ℝ)} (hA : A.Nonempty) {h : C(K, ℝ)} (hh : h ∈ upperBounds A) (x : K) : continuousFamilySupValue K A x ≤ h x

Bounds every cut value by any continuous upper bound of the family; used to prove minimality of the constructed supremum.

theorem OrderClosures.continuous_continuousFamilySupValue (K : Type u) [TopologicalSpace K] [ExtremallyDisconnected K] {A : Set C(K, ℝ)} (hA : A.Nonempty) (hAbdd : BddAbove A) : Continuous (continuousFamilySupValue K A)

Proves continuity of the cut-defined supremum value; this allows it to be bundled as continuousFamilySup.

noncomputable def OrderClosures.continuousFamilySup (K : Type u) [TopologicalSpace K] [ExtremallyDisconnected K] (A : Set C(K, ℝ)) (hA : A.Nonempty) (hAbdd : BddAbove A) : C(K, ℝ)

Bundles the cut-defined pointwise supremum as a continuous function; used to prove order completeness of the continuous-function lattice.

Equations

• OrderClosures.continuousFamilySup K A hA hAbdd = { toFun := OrderClosures.continuousFamilySupValue K A, continuous_toFun := ⋯ }

theorem OrderClosures.continuousFamilySup_isLUB (K : Type u) [TopologicalSpace K] [ExtremallyDisconnected K] (A : Set C(K, ℝ)) (hA : A.Nonempty) (hAbdd : BddAbove A) : IsLUB A (continuousFamilySup K A hA hAbdd)

Verifies that the constructed continuous function is the least upper bound of the family; used to prove order completeness of C(K, ℝ).

theorem OrderClosures.isOrderComplete_continuousMap (K : Type u) [TopologicalSpace K] [ExtremallyDisconnected K] : IsOrderComplete C(K, ℝ)

Packages the continuous-family supremum construction as order completeness of continuous real functions on an extremally disconnected compact space.

noncomputable def OrderClosures.clopenIndicator (K : Type u) [TopologicalSpace K] (s : Set K) (hs : IsClopen s) : C(K, ℝ)

The continuous zero-one indicator of a clopen set; used to embed Boolean clopens into the vector lattice of continuous functions.

Equations

• OrderClosures.clopenIndicator K s hs = { toFun := s.indicator 1, continuous_toFun := ⋯ }

@[simp]

theorem OrderClosures.clopenIndicator_apply_mem (K : Type u) [TopologicalSpace K] (s : Set K) (hs : IsClopen s) {x : K} (hx : x ∈ s) : (clopenIndicator K s hs) x = 1

@[simp]

theorem OrderClosures.clopenIndicator_apply_notMem (K : Type u) [TopologicalSpace K] (s : Set K) (hs : IsClopen s) {x : K} (hx : x ∉ s) : (clopenIndicator K s hs) x = 0

@[simp]

theorem OrderClosures.clopenIndicator_empty (K : Type u) [TopologicalSpace K] : clopenIndicator K ∅ ⋯ = 0

theorem OrderClosures.clopenIndicator_inter (K : Type u) [TopologicalSpace K] (s t : Set K) (hs : IsClopen s) (ht : IsClopen t) : clopenIndicator K (s ∩ t) ⋯ = clopenIndicator K s hs ⊓ clopenIndicator K t ht

Computes the infimum of two clopen indicators; used to make Boolean indicators compatible with lattice operations.

theorem OrderClosures.clopenIndicator_union (K : Type u) [TopologicalSpace K] (s t : Set K) (hs : IsClopen s) (ht : IsClopen t) : clopenIndicator K (s ∪ t) ⋯ = clopenIndicator K s hs ⊔ clopenIndicator K t ht

Computes the supremum of two clopen indicators; used in the Boolean-to- vector-sublattice transfer.

theorem OrderClosures.clopenIndicator_compl (K : Type u) [TopologicalSpace K] (s : Set K) (hs : IsClopen s) : clopenIndicator K sᶜ ⋯ = 1 - clopenIndicator K s hs

Computes the indicator of a clopen complement; used to recover Boolean complements inside a vector sublattice.

noncomputable def OrderClosures.booleanStoneIndicator (B : Type u) [CompleteBooleanAlgebra B] (b : B) : C(BooleanStone B, ℝ)

The continuous indicator associated with a Boolean element under Stone duality; used as the Boolean generator inside the vector lattice.

Equations

• OrderClosures.booleanStoneIndicator B b = OrderClosures.clopenIndicator (OrderClosures.BooleanStone B) (OrderClosures.booleanStoneClopen B b) ⋯

@[simp]

theorem OrderClosures.booleanStoneIndicator_apply (B : Type u) [CompleteBooleanAlgebra B] (b : B) (x : BooleanStone B) : (booleanStoneIndicator B b) x = if ↑x b = true then 1 else 0

@[simp]

theorem OrderClosures.booleanStoneIndicator_bot (B : Type u) [CompleteBooleanAlgebra B] : booleanStoneIndicator B ⊥ = 0

@[simp]

theorem OrderClosures.booleanStoneIndicator_inf (B : Type u) [CompleteBooleanAlgebra B] (a b : B) : booleanStoneIndicator B (a ⊓ b) = booleanStoneIndicator B a ⊓ booleanStoneIndicator B b

@[simp]

theorem OrderClosures.booleanStoneIndicator_sup (B : Type u) [CompleteBooleanAlgebra B] (a b : B) : booleanStoneIndicator B (a ⊔ b) = booleanStoneIndicator B a ⊔ booleanStoneIndicator B b

@[simp]

theorem OrderClosures.booleanStoneIndicator_compl (B : Type u) [CompleteBooleanAlgebra B] (a : B) : booleanStoneIndicator B aᶜ = 1 - booleanStoneIndicator B a

theorem OrderClosures.booleanStoneClopen_sSup (B : Type u) [CompleteBooleanAlgebra B] (S : Set B) : booleanStoneClopen B (sSup S) = closure (⋃ b ∈ S, booleanStoneClopen B b)

Shows that arbitrary Boolean suprema correspond to closures of unions of Stone clopens; used to transfer completeness into vector sublattices.

theorem OrderClosures.booleanStoneIndicator_mono (B : Type u) [CompleteBooleanAlgebra B] {a b : B} (hab : a ≤ b) : booleanStoneIndicator B a ≤ booleanStoneIndicator B b

Transfers Boolean order to order between indicator functions; used in order-convergence and sublattice generation arguments.

theorem OrderClosures.booleanStoneIndicator_nonneg (B : Type u) [CompleteBooleanAlgebra B] (a : B) : 0 ≤ booleanStoneIndicator B a

Records positivity of Boolean Stone indicators; used when constructing monotone order-convergent families.

noncomputable def OrderClosures.booleanSubalgebraInVectorSublattice (B : Type u) [CompleteBooleanAlgebra B] (Z : VectorSublattice C(BooleanStone B, ℝ)) (hOne : 1 ∈ Z) : BooleanSubalgebra B

Boolean elements whose Stone indicators lie in a fixed vector sublattice; used to transfer complete Boolean generation to vector-lattice generation.

Equations

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

theorem OrderClosures.booleanSubalgebraInVectorSublattice_complete (B : Type u) [CompleteBooleanAlgebra B] (Z : VectorSublattice C(BooleanStone B, ℝ)) (hOne : 1 ∈ Z) (hZclosed : IsOrderClosed ↑Z) : IsCompleteBooleanSubalgebra (booleanSubalgebraInVectorSublattice B Z hOne)

Shows that Boolean elements whose indicators lie in a vector sublattice form a complete Boolean subalgebra; used with Solovay generation for maximality.

theorem OrderClosures.continuousMap_orderConvergesTo_of_tendsto {K : Type u} [TopologicalSpace K] [CompactSpace K] {ι : Type v} [Preorder ι] {f : ι → C(K, ℝ)} {x : C(K, ℝ)} (hfx : Filter.Tendsto f Filter.atTop (nhds x)) : OrderConvergesTo f x

Converts uniform convergence with a summable error bound into order convergence; used to show order-closed sublattices are norm closed.

theorem OrderClosures.isClosed_of_isOrderClosed_vectorSublattice {K : Type u} [TopologicalSpace K] [CompactSpace K] (Z : VectorSublattice C(K, ℝ)) (hZ : IsOrderClosed ↑Z) : IsClosed ↑Z

Derives norm closedness of a vector sublattice from order closedness; used to compare the closed separable sublattice with larger order-closed ones.

theorem OrderClosures.booleanStoneIndicators_separateStrongly (B : Type u) [CompleteBooleanAlgebra B] (Z : VectorSublattice C(BooleanStone B, ℝ)) (hOne : 1 ∈ Z) (hIndicator : ∀ (b : B), booleanStoneIndicator B b ∈ Z) : (↑Z).SeparatesPointsStrongly

Produces a Boolean indicator separating two distinct Stone points; used in the lattice Stone--Weierstrass argument.

theorem OrderClosures.vectorSublattice_eq_top_of_booleanStoneIndicators (B : Type u) [CompleteBooleanAlgebra B] (Z : VectorSublattice C(BooleanStone B, ℝ)) (hOne : 1 ∈ Z) (hIndicator : ∀ (b : B), booleanStoneIndicator B b ∈ Z) (hZorder : IsOrderClosed ↑Z) : Z = ⊤

Shows that a closed vector sublattice containing every Boolean indicator is all of C(K, ℝ); used to prove maximality of the Solovay sublattice.

theorem OrderClosures.cardinalMk_le_densityCharacter_of_oneSeparated {A X : Type u} [PseudoMetricSpace X] (e : A → X) (hsep : ∀ (a b : A), a ≠ b → 1 ≤ dist (e a) (e b)) : Cardinal.mk A ≤ densityCharacter X

Bounds density character below by the cardinality of a one-separated family; used for the Stone-space continuous-function density estimate.

theorem OrderClosures.one_le_dist_booleanStoneIndicator (B : Type u) [CompleteBooleanAlgebra B] {a b : B} (hab : a ≠ b) : 1 ≤ dist (booleanStoneIndicator B a) (booleanStoneIndicator B b)

Shows distinct Boolean elements give indicators at distance at least one; used to obtain a large separated family.

theorem OrderClosures.cardinalMk_le_densityCharacter_booleanStoneContinuousMap (B : Type u) [CompleteBooleanAlgebra B] : Cardinal.mk B ≤ densityCharacter C(BooleanStone B, ℝ)

Transfers the size of a Boolean algebra to a lower bound on the density character of its continuous-function lattice.

noncomputable def OrderClosures.solovayVectorGenerators (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] : Set C(BooleanStone (RegularOpen (SolovayProduct Gamma)), ℝ)

A countable selection of Boolean Stone indicators generating the Solovay vector sublattice used in the Gao counterexample.

Equations

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

noncomputable def OrderClosures.solovayVectorSublattice (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] : VectorSublattice C(BooleanStone (RegularOpen (SolovayProduct Gamma)), ℝ)

The closed vector sublattice generated by the selected Solovay indicators; this is the separable maximal order-closed witness.

Equations

• OrderClosures.solovayVectorSublattice Gamma = (VectorSublattice.generated (OrderClosures.solovayVectorGenerators Gamma)).topologicalClosure

theorem OrderClosures.solovayVectorGenerators_countable (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] : (solovayVectorGenerators Gamma).Countable

Records countability of the selected vector generators; used to prove separability of their closed generated sublattice.

theorem OrderClosures.solovayVectorGenerator_mem (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] {f : C(BooleanStone (RegularOpen (SolovayProduct Gamma)), ℝ)} (hf : f ∈ solovayVectorGenerators Gamma) : f ∈ solovayVectorSublattice Gamma

Places each selected generator in the Solovay vector sublattice; used to show that any containing sublattice contains the generated Boolean algebra.

theorem OrderClosures.isClosed_solovayVectorSublattice (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] : IsClosed ↑(solovayVectorSublattice Gamma)

Records closedness of the generated Solovay vector sublattice; this is one of the properties required by gao_counterexample.

theorem OrderClosures.isSeparable_solovayVectorSublattice (Gamma : Type u) [LinearOrder Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] : TopologicalSpace.IsSeparable ↑(solovayVectorSublattice Gamma)

Derives separability from the countable generator family; this supplies the separable sublattice in gao_counterexample.

theorem OrderClosures.solovayVectorSublattice_maximalOrderClosed (Gamma : Type u) [LinearOrder Gamma] [WellFoundedLT Gamma] [TopologicalSpace Gamma] [DiscreteTopology Gamma] (Z : VectorSublattice C(BooleanStone (RegularOpen (SolovayProduct Gamma)), ℝ)) (hYZ : solovayVectorSublattice Gamma ≤ Z) (hZorder : IsOrderClosed ↑Z) : Z = ⊤

Shows that every order-closed vector sublattice containing the Solovay sublattice is the whole continuous-function lattice.