mem_closure — Mathlib

English

For x in α, x belongs to closure s iff x ∈ L for every Boolean subalgebra L that contains s.

Русский

Для x ∈ α верно: x принадлежит замыканию s тогда и только тогда, когда для любого булева подполья L, содержающего s, x ∈ L.

LaTeX

$$$x \\in \\mathrm{closure}(s) \\iff \\forall L,\\; s \\subseteq L \\Rightarrow x \\in L$$$

Lean4

theorem mem_closure {x : α} : x ∈ closure s ↔ ∀ ⦃L : BooleanSubalgebra α⦄, s ⊆ L → x ∈ L :=
  mem_sInf

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