Regularization of open sets preserves finite meets

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.regularization_preserves_meet

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

prove2quantumquantum-logicregular-open-setsstone-duality

For any topological space and any two open sets U,V, regularization j(U)=int(cl U) satisfies

j(U\cap V)=j(U)\cap j(V).

This is the double-pseudocomplement finite-meet law for the open-set lattice. No separation or compactness assumption is required. It supplies the filter-intersection step in the Stone-spectrum regularization correspondence.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
noncomputable section
open Set TopologicalSpace
universe u

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem regularization_preserves_meet {M : Type u} [TopologicalSpace M] (U V : Opens M) :
    regularizeOpen (U ⊓ V) = regularizeOpen U ⊓ regularizeOpen V := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20

Source

Hans F. de Groote, Observables I: Stone Spectra, arXiv:math-ph/0509020v1, https://arxiv.org/pdf/math-ph/0509020v1, Section 2.1, printed pp.17–18, regular open sets and pseudocomplements; Section 3.3, Lemma 3.4 and Proposition 3.16, printed pp.54–55 (PDF pp.55–56).

View graph