A quasipoint containing a restricts to a quasipoint of the principal ideal

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.quasipoint_restrict_principal_ideal

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

lattice-theoryquantum-logicstone-duality

Let $L$ be a bounded lattice, let $a\in L$ , and let $B$ be a quasipoint with $a\in B$ . For the principal ideal $L_a=\{b:b\le a\}$ , with its inherited order and least element $0$ , the restriction

B|_{L_a}=\{b\in L_a:b\in B\}

is a quasipoint of the principal ideal. This is the well-definedness step for restricting the Stone spectrum to the basic open Q_a.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem quasipoint_restrict_principal_ideal {L : Type*} [Lattice L] [BoundedOrder L]
    (a : L) (B : StoneSpectrum L) (hBa : a ∈ B.val) :
    letI : Bot (Set.Iic a) := ⟨⟨⊥, bot_le⟩⟩
    IsQuasipoint {b : Set.Iic a | b.val ∈ B.val} := 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, proof of Proposition 3.21, printed p.65 (PDF p.66): the principal-ideal Stone spectrum is homeomorphic to Q_a. This supporting lemma isolates the restriction map.

View graph