Proposition 3.8

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.open_quasipoint_dichotomy

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

prove2quantum

For a locally compact Hausdorff space $M$ and a quasipoint $\mathfrak B$ of its open-set lattice, exactly one of the following occurs: every complement of a compact set belongs to $\mathfrak B$ ; or there is a unique $x\in M$ with

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

These are respectively the unbounded quasipoints and the bounded quasipoints over a point. A bounded quasipoint need not equal the ordinary neighbourhood filter.

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.8; de Groote, Observables I, PDF p./pp. 49.
-/
theorem open_quasipoint_dichotomy {M : Type u} [TopologicalSpace M] [LocallyCompactSpace M] [T2Space M]
    (B : StoneSpectrum (Opens M)) :
    ((∀ K : Set M, IsCompact K → ∃ U ∈ B.val, (U : Set M) = Kᶜ) ∧
      ¬ ∃ x : M, LiesOver B x) ∨
    ((∃! x : M, LiesOver B x) ∧
      ¬ (∀ K : Set M, IsCompact K → ∃ U ∈ B.val, (U : Set M) = Kᶜ)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

Read-back

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

Let $M$ be a locally compact Hausdorff 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$ . Say that $B$ lies over $x\in M$ when $\bigcap_{U\in B}\overline U=\{x\}$ . Then either every compact subset $K\subseteq M$ has an open complement belonging to $B$ , in the precise sense that there exists $U\in B$ with $U=M\setminus K$ , and there is no $x\in M$ over which $B$ lies; or there exists exactly one $x\in M$ over which $B$ lies, and it is false that every compact $K\subseteq M$ admits $U\in B$ with $U=M\setminus K$ . The assertion is conditional on such a family $B$ being given; no such family exists when $M=\varnothing$ .

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