Lemma 3.5

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.open_dual_ideal_quasipoint_alternative

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

prove2quantum

A proper dual ideal $J$ in the open-set lattice of any space $M$ is a quasipoint exactly when

\forall U\in T(M),\qquad U\in J\ \text{or}\ M\setminus\overline U\in J.

The second set is the open pseudocomplement, not the ordinary complement of $U$ .

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

/-- Lemma 3.5; de Groote, Observables I, PDF p./pp. 58.
-/
theorem open_dual_ideal_quasipoint_alternative {M : Type u} [TopologicalSpace M] (J : Set (Opens M)) (hJ : IsDualIdeal J) :
    IsQuasipoint J ↔ ∀ U : Opens M, U ∈ J ∨ openPseudoCompl U ∈ J := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 58, Lemma 3.5

Read-back

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

Let $M$ be any topological space, and let $J$ be a nonempty family of open subsets of $M$ that excludes $\varnothing$ , is upward closed among open sets under inclusion, and is closed under binary intersections. Then $J$ is a quasipoint—meaning that it is a nonempty family excluding $\varnothing$ , every two members contain a common member of $J$ , and it is maximal under inclusion among families of open sets with these properties—if and only if, for every open subset $U\subseteq M$ ,

U\in J\quad\text{or}\quad M\setminus\overline U\in J.

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