isAtom — Mathlib

English

An ultrafilter is an atom in the lattice of filters: its atomhood is expressed by Ultrafilter.isAtom.

Русский

Ульрафильтр является атомом в решетке фильтров: атомность формализована как Ultrafilter.isAtom.

LaTeX

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

Lean4

protected theorem isAtom (f : Ultrafilter α) : IsAtom (f : Filter α) :=
  ⟨f.neBot.ne, fun _ hgf => by_contra fun hg => hgf.ne <| f.unique hgf.le ⟨hg⟩⟩

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