rem-3.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.ideal_avoidance_iff_complements

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

prove2quantum

Let $I$ be a sigma ideal in a countably complete Boolean algebra $L$ and let $\mathfrak B$ be a quasipoint. Then

\mathfrak B\cap I=\varnothing\quad\Longleftrightarrow\quad \{a^\perp:a\in I\}\subseteq\mathfrak B.

The quasipoint hypothesis is essential; this equivalence is not claimed for arbitrary subsets.

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

/-- rem-3.2; de Groote, Observables I, PDF p./pp. 54.
-/
theorem ideal_avoidance_iff_complements {L : Type u} [BooleanAlgebra L] (hcomplete : IsSigmaComplete L)
    (I : Set L) (hI : IsSigmaIdeal I) (B : StoneSpectrum L) :
    B.val ∩ I = ∅ ↔ (fun a : L => aᶜ) '' I ⊆ B.val := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 54, rem-3.2

Read-back

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

Let $L$ be a Boolean algebra in which every sequence has a least upper bound. Let $I\subseteq L$ be nonempty and downward closed, and suppose that for every sequence $(a_n)_{n\in\mathbb N}$ with all $a_n\in I$ , every least upper bound of its range belongs to $I$ . Let $B\subseteq L$ be an inclusion-maximal nonempty subset excluding $\bot$ in which any two members have a common lower bound belonging to $B$ . Then

B\cap I=\varnothing \quad\Longleftrightarrow\quad \{a^{\mathrm c}:a\in I\}\subseteq B,

where $a^{\mathrm c}$ is the Boolean complement of $a$ . There is no assumption that $I$ is proper; $I=L$ is included.

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