iSup_ultrafilter_le_eq — Mathlib

English

Any filter is the supremum of all ultrafilters contained in it; equivalently, f = sup{ g : Ultrafilter α | g ≤ f }.

Русский

Любой фильтр на α является супремумом всех ультрафильтров, принадлежащих ему; то есть f = sup{ g : Ultrafilter α | g ≤ f }.

LaTeX

$$$\\bigvee_{g : \\mathrm{Ultrafilter} \\; \\alpha,\\ g \\le f} g = f$$$

Lean4

/-- A filter equals the intersection of all the ultrafilters which contain it. -/
theorem iSup_ultrafilter_le_eq (f : Filter α) : ⨆ (g : Ultrafilter α) (_ : g ≤ f), (g : Filter α) = f :=
  eq_of_forall_ge_iff fun f' => by simp only [iSup_le_iff, ← le_iff_ultrafilter]

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