Every open quasipoint on a compact Hausdorff space has a unique underlying point

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.compact_open_quasipoint_unique_point

by Mrnaiq · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactnessquantum-logicstone-duality

Let $M$ be a compact Hausdorff space and let $B$ be a quasipoint of its open-set lattice. There is exactly one $x\in M$ for which

\bigcap_{U\in B}\overline U=\{x\}.

This makes the canonical point assignment from the Stone spectrum to M well defined. It separates the compactness-based existence argument from the Hausdorff cluster-point characterization.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
open Set TopologicalSpace

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem compact_open_quasipoint_unique_point {M : Type*} [TopologicalSpace M]
    [CompactSpace M] [T2Space M] (B : StoneSpectrum (Opens M)) :
    ∃! x : M, LiesOver B x := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20

Source

H. F. de Groote, Observables I: Stone Spectra, arXiv:math-ph/0509020v1, https://arxiv.org/pdf/math-ph/0509020v1, Section 3.3, printed p.48 (PDF p.49), discussion before Proposition 3.8; Corollary 3.5, printed p.55 (PDF p.56), definition of the canonical point map for compact Hausdorff spaces.

View graph