instIsAtomicFilter — Mathlib

English

The lattice of filters is atomic: every filter contains an atom below it, realized by an ultrafilter.

Русский

Число фильтров образуют атомарную решетку: каждый фильтр содержит атом ниже себя, который задается ульрафильтром.

LaTeX

$$$\text{Filter }(\alpha) \text{ is atomic: } \forall F, \exists U\le F \text{ with } U \text{ an ultrafilter below } F$$$

Lean4

/-- `Filter α` is an atomic type: for every filter there exists an ultrafilter that is less than or
equal to this filter. -/
instance : IsAtomic (Filter α) :=
  IsAtomic.of_isChain_bounded fun c hc hne hb =>
    ⟨sInf c, (sInf_neBot_of_directed' hne (show IsChain (· ≥ ·) c from hc.symm).directedOn hb).ne, fun _ hx =>
      sInf_le hx⟩

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