Lemma 3.4

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.regularized_base_is_quasipoint

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

prove2quantum

For every topological space $M$ and quasipoint $\mathfrak B\in Q(T(M))$ , regularization produces a quasipoint in the regular-open Boolean algebra:

\mathfrak B^r=\{\operatorname{int}\overline U:U\in\mathfrak B\}\in Q(T_r(M)).

No separation, compactness or Baire hypothesis is imposed.

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

/-- Lemma 3.4; de Groote, Observables I, PDF p./pp. 56.
-/
theorem regularized_base_is_quasipoint {M : Type u} [TopologicalSpace M] (B : StoneSpectrum (Opens M)) :
    IsQuasipoint (regularizedBase B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 56, Lemma 3.4

Read-back

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

Let $M$ be any topological space, and let $B$ be an inclusion-maximal nonempty family of open subsets of $M$ that excludes $\varnothing$ and such that any two members contain a common member of $B$ . A regular open set is an open subset $V\subseteq M$ satisfying $\operatorname{int}(\overline V)=V$ ; order these sets by inclusion and take $\varnothing$ as bottom. Then the family

R_B=\{V\subseteq M:V\text{ is regular open and }\exists U\in B,\ \operatorname{int}(\overline U)=V\}

is nonempty, excludes $\varnothing$ , and has the property that any two of its members contain a common member of $R_B$ ; moreover, every family $C$ of regular open sets with these same three properties and satisfying $R_B\subseteq C$ equals $R_B$ . No separation assumption is imposed on $M$ .

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