quasipoint-extension

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.filter_base_extends_to_quasipoint

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

prove2quantum

Every proper nonempty filter base $B$ in a bounded lattice $L$ extends to a quasipoint:

\exists\mathfrak B\in Q(L),\qquad B\subseteq\mathfrak B.

This supplies existence from the base itself rather than adding existence of quasipoints as a hypothesis.

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

/-- quasipoint-extension; de Groote, Observables I, PDF p./pp. 39.
-/
theorem filter_base_extends_to_quasipoint {L : Type u} [Lattice L] [BoundedOrder L] (B : Set L) (hB : IsFilterBase B) :
    ∃ C : Set L, IsQuasipoint C ∧ B ⊆ C := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 39, quasipoint-extension

Read-back

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

Let $L$ be any bounded lattice, and let $B\subseteq L$ be nonempty, exclude $\bot$ , and satisfy the condition that for every $a,b\in B$ there is $c\in B$ with $c\le a$ and $c\le b$ . Then there exists a set $C\subseteq L$ containing $B$ such that $C$ is nonempty, excludes $\bot$ , has this same common-lower-bound property, and is maximal under inclusion among sets with these properties: every such set $D$ with $C\subseteq D$ equals $C$ . No uniqueness of $C$ is asserted. If $L$ has $\bot=\top$ , no $B$ satisfies the hypotheses.

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