## Stream: Is there code for X?

### Topic: is_open_iff_ultrafilter

#### 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


#### Adam Topaz (Oct 08 2020 at 02:04):

It's actually true....

#### Kevin Buzzard (Oct 08 2020 at 06:23):

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

#### Yury G. Kudryashov (Oct 08 2020 at 08:22):

I'll PR a short proof soon.

#### Yury G. Kudryashov (Oct 08 2020 at 08:25):

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

#### Yury G. Kudryashov (Oct 08 2020 at 08:25):

It was easier to prove this way.

#### 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