closure-basic-union

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.closure_of_basic_union

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

prove2quantum

For any family represented by a subset $S$ of a bounded lattice,

\mathfrak B\in\overline{\bigcup_{a\in S}Q_a}\quad\Longleftrightarrow\quad \forall b\in\mathfrak B\ \exists a\in S:\ b\wedge a\ne0.

Empty families are allowed. The closure bar is essential. The complete-frame strengthening (3.4) is included in the separate Proposition 3.7 statement.

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

/-- closure-basic-union; de Groote, Observables I, PDF p./pp. 45.
-/
theorem closure_of_basic_union {L : Type u} [Lattice L] [BoundedOrder L] (s : Set L) (B : StoneSpectrum L) :
    (B ∈ closure (⋃ a ∈ s, stoneBasic a) ↔ ∀ b ∈ B.val, ∃ a ∈ s, b ⊓ a ≠ ⊥) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 45, closure-basic-union

Read-back

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

Let $L$ be any bounded lattice. Let $\mathcal Q(L)$ consist of the inclusion-maximal nonempty subsets $B\subseteq L$ excluding $\bot$ such that any two members have a common lower bound belonging to $B$ , and equip $\mathcal Q(L)$ with the topology generated by $D(a)=\{C\in\mathcal Q(L):a\in C\}$ . For every subset $s\subseteq L$ and every $B\in\mathcal Q(L)$ , $B$ belongs to the closure of $\bigcup_{a\in s}D(a)$ if and only if, for every $b\in B$ , there exists $a\in s$ with $b\wedge a\ne\bot$ . The subset $s$ may be empty; in that case the union and its closure are empty, and the right-hand condition is false because $B$ is nonempty.

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