exists_ultrafilter_iff — Mathlib

English

There exists an ultrafilter below a filter f if and only if f is nonempty (NeBot).

Русский

Существует ультрафильтр ниже фильтра f тогда и только тогда, когда f не пустой (NeBot).

LaTeX

$$$(\\exists u : \\mathrm{Ultrafilter} \\; \\alpha,\\ u \\le f) \\iff \\mathrm{NeBot}(f)$$$

Lean4

theorem exists_ultrafilter_iff {f : Filter α} : (∃ u : Ultrafilter α, ↑u ≤ f) ↔ NeBot f :=
  ⟨fun ⟨_, uf⟩ => neBot_of_le uf, fun h => @exists_ultrafilter_le _ _ h⟩

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