A Stone basic open is nonempty exactly when its element is nonzero

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.stoneBasic_nonempty_iff

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

lattice-theoryquantum-foundationsquantum-logicstone-duality

Let $L$ be a bounded lattice and let $Q_a$ be the set of quasipoints containing $a$ . Then

Q_a\ne\varnothing\quad\Longleftrightarrow\quad a\ne0.

This identifies nonzero lattice elements with nonempty basic neighborhoods. It is a supporting lemma for the characterization of closures of unions of Stone basic sets.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

theorem stoneBasic_nonempty_iff {L : Type*} [Lattice L] [BoundedOrder L] (a : L) :
    (stoneBasic a).Nonempty ↔ a ≠ ⊥ := 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.1, printed pp.38–39 (Zorn extension and the definition of Q_a); Section 3.2, printed p.44, the equivalence immediately before Proposition 3.7.

View graph