The upward closure of a proper filter base is a proper filter base

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.filter_base_upward_closure

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

lattice-theoryquantum-logicstone-duality

Let $L$ be a partially ordered set with least element $0$ , and let $B\subseteq L$ be a proper nonempty directed filter base. Its upward closure

\uparrow B=\{x\in L:\exists b\in B,\ b\le x\}

is again a proper nonempty directed filter base. This basic extension operation supports the restriction and extension of quasipoints along principal ideals, and does not require lattice operations.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem filter_base_upward_closure {L : Type*} [PartialOrder L] [OrderBot L]
    (B : Set L) (hB : IsFilterBase B) :
    IsFilterBase {x : L | ∃ b ∈ B, b ≤ x} := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20

Source

Supporting filter-base lemma for H. F. de Groote, Observables I: Stone Spectra, arXiv:math-ph/0509020v1, https://arxiv.org/pdf/math-ph/0509020v1, Definition 3.3 and Proposition 3.4, printed pp.37–38; principal-ideal spectrum correspondence used in the proof of Proposition 3.21, printed p.65 (PDF p.66). The upward-closure operation is formalized separately here.

View graph