lim — Mathlib

English

For an ultrafilter F on X, the value lim F is a limit of F whenever such a limit exists.

Русский

Для ультрафильтра F на X число lim F является пределом F, если он существует.

LaTeX

$$$\\text{Let }F\\text{ be an ultrafilter on }X.\\;\\operatorname{Tendsto} \\mathrm{id}_X\\, F\\, (\\mathcal{N}(\\operatorname{lim} F))$$$

Lean4

/-- If `F` is an ultrafilter, then `Filter.Ultrafilter.lim F` is a limit of the filter, if it exists.
Note that dot notation `F.lim` can be used for `F : Filter.Ultrafilter X`.
-/
noncomputable nonrec def lim (F : Ultrafilter X) : X :=
  @lim X _ (nonempty_of_neBot F) F

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