instIsCoatomistic — Mathlib

English

The lattice of all subsets of α is coatomistic: every subset s equals the intersection of all coatoms that contain it, i.e., s = ⋂_{x ∉ s} (α \ {x}).

Русский

Решётка подмножеств α является котатомистической: каждое подмножество s равно пересечению всех катомов, которые содержат s, то есть s = ⋂_{x ∉ s} (α \ {x}).

LaTeX

$$$s = \\bigcap_{x \\in \\alpha \\setminus s} {x}^{c}$$$

Lean4

instance : IsCoatomistic (Set α) :=
  inferInstance

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