## Stream: maths

### Topic: ultrafilter.Lim

#### Adam Topaz (Oct 09 2020 at 14:37):

I wonder whether it makes sense to define something like the following:

def filter.ultrafilter.Lim {X : Type*} [topological_space X] : ultrafilter X  X :=
λ F, @Lim _ _ (@nonempty_of_ne_bot _ F.1 F.2.1) F.1

After #4545 there will be a few instances where one would like to take a limit of an ultrafilter, and in all those cases we have to manually tell lean that X is nonempty assuming we have F : ultrafilter X.