is_open_iff_ultrafilter

Stream: Is there code for X?

[Adam Topaz]

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]

It's actually true....

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) :=
begin
  split,
  { intros hU F x h hx,
    rw le_nhds_iff at h,
    specialize h U hx hU,
    assumption },
  { intro h,
    rw ←is_closed_compl_iff,
    suffices : closure Uᶜ ⊆ Uᶜ,
    { have : closure Uᶜ = Uᶜ,
      { ext,
        split,
        apply this,
        intro hx,
        apply subset_closure,
        assumption },
      rw ←this,
      exact is_closed_closure },
    intros x hx,
    rw mem_closure_iff_ultrafilter at hx,
    rcases hx with ⟨F,h1,h2⟩,
    specialize h F x h2,
    by_contradiction,
    have : x ∈ U, rwa ←set.not_not_mem,
    specialize h this,
    rw ultrafilter_iff_compl_mem_iff_not_mem.mp F.2 at h1,
    contradiction },
end

[Kevin Buzzard]

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

[Yury G. Kudryashov]

I'll PR a short proof soon.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

It was easier to prove this way.

[Yury G. Kudryashov]

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