Proposition 3.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.points_of_open_lattice

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

prove2quantum

Let $M$ be a regular Hausdorff space and let $p$ be a nonempty subset of its open-set lattice. Then $p$ is a lattice point, preserving arbitrary joins, if and only if

p=\{U\subseteq M:U\text{ open and }x\in U\}

for a unique $x\in M$ . Hausdorff separation makes explicit the source's regular-space convention.

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.2; de Groote, Observables I, PDF p./pp. 37.
-/
theorem points_of_open_lattice {M : Type u} [TopologicalSpace M] [RegularSpace M] [T2Space M]
    (p : Set (Opens M)) (hne : p.Nonempty) :
    IsLatticePoint p ↔ ∃! x : M, p = {U : Opens M | x ∈ (U : Set M)} := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

Read-back

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

For every regular Hausdorff topological space $M$ and every nonempty set $p$ of open subsets of $M$ , the following are equivalent: $p$ excludes $\varnothing$ , is upward closed under inclusion, is closed under binary intersections, and has the property that for every set $\mathcal U$ of open subsets, $\bigcup_{U\in\mathcal U}U\in p$ implies $U\in p$ for some $U\in\mathcal U$ ; and there exists exactly one point $x\in M$ such that $p=\{U\subseteq M:U\text{ is open and }x\in U\}$ . The union condition ranges over arbitrary families, including the empty family. No nonemptiness assumption on $M$ is made; if $M=\varnothing$ , the asserted existence of a point is false, and no allowed nonempty $p$ satisfies the conditions on the other side.

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