Proposition 3.17

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.borel_saturation_quasipoint

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a Baire space $M$ and $\mathfrak B\in Q(T(M))$ , define $C(\mathfrak B)$ to be the Borel sets differing by a meagre set from some member of $\mathfrak B$ . Then

C(\mathfrak B)\in Q(B(M)),\qquad C(\mathfrak B)\cap I_1=\varnothing,

where $I_1$ is the ideal of meagre Borel sets. The subset $C(\mathfrak B)$ is computed from $\mathfrak B$ , not supplied as additional data.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- Proposition 3.17; de Groote, Observables I, PDF p./pp. 57.
-/
theorem borel_saturation_quasipoint {M : Type u} [TopologicalSpace M] [BaireSpace M]
    (B : StoneSpectrum (Opens M)) :
    IsQuasipoint (borelSaturation B) ∧
      ∀ A ∈ borelSaturation B, ¬ IsMeagre A.val := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 57, Proposition 3.17

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $M$ be a Baire topological space, and let $B$ be a quasipoint of its open sets: $B$ is a nonempty family of open sets, excludes $\varnothing$ , contains a common lower bound under inclusion for every pair of its members, and is maximal under inclusion among families with these properties. Define

S_B=\{A\subseteq M:A\text{ is Borel and }A\mathbin{\triangle}U\text{ is meagre for some }U\in B\},

where $A\mathbin{\triangle}U=(A\setminus U)\cup(U\setminus A)$ . Then $S_B$ is a nonempty family of Borel sets excluding $\varnothing$ , every two members contain a common member of $S_B$ , and $S_B$ is maximal under inclusion among families of Borel sets with these properties. Moreover, every $A\in S_B$ is nonmeagre.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph