Zulip Chat Archive

Stream: Is there code for X?

Topic: is_open_iff_ultrafilter


view this post on Zulip Adam Topaz (Oct 08 2020 at 02:01):

Does mathlib have the following characterization of open sets?

theorem is_open_iff_ultrafilter {X : Type*} [topological_space X] (U : set X) : is_open U 
  ( (F : ultrafilter X) (x : X), F.1  nhds x  x  U  U  F.1) := sorry

view this post on Zulip Adam Topaz (Oct 08 2020 at 02:04):

It's actually true....

view this post on Zulip Kevin Buzzard (Oct 08 2020 at 06:23):

This is one of those theorems that could have some amazing two line proof

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 08:22):

I'll PR a short proof soon.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 08:25):

#4529 uses is_ultrafilter instead of ultrafilter and a different order of foralls.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 08:25):

It was easier to prove this way.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 08:26):

If you want ∀ f : ultrafilter α, then you should add lemmas like docs#subtype.forall


Last updated: May 16 2021 at 05:21 UTC