A nonmember of a quasipoint has a disjoint member

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.quasipoint_nonmember_has_disjoint_member

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

lattice-theoryquantum-foundationsquantum-logicstone-duality

Let $L$ be a lattice with least element $0$ and greatest element $1$ , and let $B$ be a quasipoint of $L$ : a maximal proper nonempty filter base. If $a\in L$ does not belong to $B$ , then

\exists b\in B,\qquad b\wedge a=0.

This separation property is used to show that the membership basic open sets of the Stone spectrum are also closed. It is reusable in Stone-spectrum separation, extension, and compactness arguments.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

theorem quasipoint_nonmember_has_disjoint_member {L : Type*} [Lattice L] [BoundedOrder L]
    (B : Set L) (hB : IsQuasipoint B) (a : L) (ha : a ∉ B) :
    ∃ b ∈ B, b ⊓ 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 p.39, unnumbered paragraph immediately before Definition 3.5.

View graph