Proposition 3.4

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.quasipoint_upward_and_meet_closed

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

prove2quantum

In a bounded lattice $L$ , every quasipoint $\mathfrak B$ is upward closed and closed under binary meets:

a\in\mathfrak B,\ a\le b\ \Longrightarrow\ b\in\mathfrak B, \qquad a,b\in\mathfrak B\ \Longrightarrow\ a\wedge b\in\mathfrak B.

These are consequences of maximality; they are not included in the filter-base definition.

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

/-- Proposition 3.4; de Groote, Observables I, PDF p./pp. 39.
-/
theorem quasipoint_upward_and_meet_closed {L : Type u} [Lattice L] [BoundedOrder L] (B : Set L) (hB : IsQuasipoint B) :
    (∀ a ∈ B, ∀ b : L, a ≤ b → b ∈ B) ∧
      (∀ a ∈ B, ∀ b ∈ B, a ⊓ b ∈ B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

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 a quasipoint: $B$ is nonempty, $\bot\notin B$ , for every $a,b\in B$ there is $c\in B$ with $c\le a$ and $c\le b$ , and every set $C\subseteq L$ satisfying these same three conditions and containing $B$ equals $B$ . Then $B$ is upward closed, meaning that $a\in B$ and $a\le b$ imply $b\in B$ for every $a,b\in L$ , and $B$ is closed under binary meets, meaning that $a,b\in B$ imply $a\wedge b\in B$ .

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