ultrafilter_of — Mathlib

English

If a filter f is Cauchy, then its associated ultrafilter Ultrafilter.of f is also Cauchy.

Русский

Если фильтр f является Коши, то его ассоциированный ультрафильтр Ultrafilter.of f также является Коши.

LaTeX

$$$ Cauchy(f) \Rightarrow Cauchy( Ultrafilter.of(f) )$$$

Lean4

theorem ultrafilter_of {l : Filter α} (h : Cauchy l) : Cauchy (@Ultrafilter.of _ l h.1 : Filter α) :=
  by
  haveI := h.1
  have := Ultrafilter.of_le l
  exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

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