closure — Mathlib

English

The closure of a set s in α is the smallest Boolean subalgebra of α containing s, i.e., the infimum of all Boolean subalgebras L with s ⊆ L.

Русский

Замыкание множества s в α есть наименьшее булево подполье α, содержащее s; равносильно наименьшему пределу всех подпольев L с s ⊆ L.

LaTeX

$$$\\operatorname{closure}(s) = \\bigwedge \\{ L \\mid s \\subseteq L \\}$$$

Lean4

/-- The minimum Boolean subalgebra containing a given set. -/
def closure (s : Set α) : BooleanSubalgebra α :=
  sInf {L | s ⊆ L}

Похожие утверждения