unbounded-quasipoints-compactification

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.unbounded_quasipoints_over_infinity

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

prove2quantum

Let $M$ be a noncompact locally compact Hausdorff space and $M_\infty$ its one-point compactification. A quasipoint $\mathfrak B$ has the canonical extension

\widetilde{\mathfrak B}=\{V\in T(M_\infty):V\cap M\in\mathfrak B\}.

This is a quasipoint of $T(M_\infty)$ and lies over $\infty$ exactly when $\mathfrak B$ is unbounded. The extension is defined by restriction along the canonical inclusion of $M$ .

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

/-- unbounded-quasipoints-compactification; de Groote, Observables I, PDF p./pp. 49.
-/
theorem unbounded_quasipoints_over_infinity {M : Type u} [TopologicalSpace M] [LocallyCompactSpace M] [T2Space M]
    (hnoncompact : ¬ CompactSpace M) (B : StoneSpectrum (Opens M)) :
    ∃ C : StoneSpectrum (Opens (OnePoint M)), C.val = compactificationBase B ∧
      (LiesOver C OnePoint.infty ↔ IsUnboundedQuasipoint B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 49, unbounded-quasipoints-compactification

Read-back

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

Let $M$ be a locally compact Hausdorff topological space that is not compact, 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$ . Write $M^\infty=M\cup\{\infty\}$ for its one-point compactification and $\iota:M\to M^\infty$ for the canonical inclusion. There exists an inclusion-maximal nonempty family $C$ of open subsets of $M^\infty$ that excludes $\varnothing$ and such that any two members contain a common member of $C$ , with

C=\{V\subseteq M^\infty:V\text{ is open and }\exists U\in B,\ U=\iota^{-1}(V)\},

and this $C$ satisfies

\bigcap_{V\in C}\overline V^{\,M^\infty}=\{\infty\} \quad\Longleftrightarrow\quad \forall K\subseteq M,\ K\text{ compact}\ \Longrightarrow\ \exists U\in B,\ U=M\setminus K.

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