ofAtom — Mathlib

English

If a filter f is an atom, then it yields an ultrafilter via the given construction.

Русский

Если фильтр f является атомом, то он порождает ульрафильтр посредством данной конструкции.

LaTeX

$$$\\\\mathrm{ofAtom} : \\\\mathrm{Filter}(\\\\alpha) \\\\to \\\\mathrm{IsAtom}(\\\\mathrm{f}) \\\\to \\\\mathrm{Ultrafilter}(\\\\alpha)$$$

Lean4

/-- If `f : Filter α` is an atom, then it is an ultrafilter. -/
def ofAtom (f : Filter α) (hf : IsAtom f) : Ultrafilter α
    where
  toFilter := f
  neBot' := ⟨hf.1⟩
  le_of_le g hg := (isAtom_iff_le_of_ge.1 hf).2 g hg.ne

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