doc-next-gen

Mathlib.Topology.Defs.Ultrafilter

Module docstring

{"# Limit of an ultrafilter.

  • Ultrafilter.lim f: a limit of an ultrafilter f, defined as the limit of (f : Filter X) with a proof of Nonempty X deduced from existence of an ultrafilter on X.

"}

Ultrafilter.lim definition
(F : Ultrafilter X) : X
Full source 
/--
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 Ultrafilter.lim (F : Ultrafilter X) : X :=
  @lim X _ (nonempty_of_neBot F) F
Limit of an ultrafilter
Informal description
For an ultrafilter \( F \) on a type \( X \), the limit \( \text{lim } F \) is an element of \( X \) that serves as a limit point of the filter \( F \), provided such a limit exists. The existence of an ultrafilter on \( X \) ensures that \( X \) is nonempty.