ultrafilter.Lim

Stream: maths

[Adam Topaz]

Continuing from the discussion here:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/More.20point.20set.20topology.20questions/near/212748220

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.

Any thoughts about this?

[Adam Topaz]

Alternatively:

def filter.Lim (f : filter α) [ne_bot f] : α := @Lim _ _ (nonempty_of_ne_bot f) f