Zulip Chat Archive

Stream: maths

Topic: ultrafilter.Lim


view this post on Zulip Adam Topaz (Oct 09 2020 at 14:37):

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?

view this post on Zulip Adam Topaz (Oct 09 2020 at 15:08):

Alternatively:

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

Last updated: May 10 2021 at 07:15 UTC