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.

noncomputable def Ultrafilter.lim {X : Type u_1} [TopologicalSpace X] (F : Ultrafilter X) : X

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.

Equations

• F.lim = (↑F).lim