exists_le — Mathlib

English

The ultrafilter lemma: Every proper filter is contained in an ultrafilter.

Русский

Лемма об ультрафильтре: любой правильный фильтр содержится в ультрафильтре.

LaTeX

$$$ \exists u : Ultrafilter \alpha, \uparrow u \le f $$$

Lean4

/-- The ultrafilter lemma: Any proper filter is contained in an ultrafilter. -/
theorem exists_le (f : Filter α) [h : NeBot f] : ∃ u : Ultrafilter α, ↑u ≤ f :=
  let ⟨u, hu, huf⟩ := (eq_bot_or_exists_atom_le f).resolve_left h.ne
  ⟨ofAtom u hu, huf⟩

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