is_open_set_of_eventually_nhds_within

Stream: Is there code for X?

[Vincent Beffara]

Do we have this in mathlib?

lemma is_open_set_of_eventually_nhds_within [α : Type*] [topological_space α] [t1_space α]
  {p : α → Prop} : is_open {x | ∀ᶠ y in 𝓝[≠] x, p y} :=
begin
  simp only [is_open_iff_mem_nhds, eventually_nhds_within_iff, _root_.eventually_nhds_iff],
  rintro z ⟨t, ht1, ht2, ht3⟩,
  refine filter.mem_of_superset (ht2 z ht3) (λ a ha, _),
  by_cases a = z,
  { subst h; exact ⟨t, ht1, ht2, ht3⟩ },
  { refine ⟨t ∩ {z}ᶜ, _, _, _⟩,
    { exact λ x ⟨hx1, hx2⟩ hx3, ht1 x hx1 hx2 },
    { exact λ x ⟨hx1, hx2⟩, filter.inter_mem (ht2 x hx1) (is_open_compl_singleton.mem_nhds hx2) },
    { exact ⟨ha, h⟩ } },
end

(Also, I would like to know how to golf the proof and possibly whether [t1_space α] is really needed, it does not feel absurd to have it but I don't have a good intuition about this.)

[Anatole Dedecker]

Here is a cleaner proof with the same assumptions

import topology.continuous_on
import topology.separation

open_locale topological_space

lemma is_open_set_of_eventually_nhds_within' [α : Type*] [topological_space α] [t1_space α]
  {p : α → Prop} : is_open {x | ∀ᶠ y in 𝓝[≠] x, p y} :=
begin
  rw is_open_iff_mem_nhds,
  intros a ha,
  filter_upwards [eventually_nhds_nhds_within.mpr ha] with b hb,
  rcases eq_or_ne a b with (h | h),
  { subst h, exact ha },
  { rw h.symm.nhds_within_compl_singleton at hb,
    exact eventually_nhds_within_of_eventually_nhds hb }
end

I'll have to think more about removing t1_space

[Vincent Beffara]

Ah, thanks! Basically I was reproving ne.nhds_within_compl_singleton which I missed from the library. (And the fact that this lemma also depends on t1_space is kind of reassuring.)

[Junyan Xu]

A T0 counterexample is the affine line: an infinite space with a distinguished "generic" point whose nonempty open sets are cofinite sets containing the generic point. If you take p to be true at all points except at the generic point, then {x | ∀ᶠ y in 𝓝[≠] x, p y} is the singleton {generic point}, which is not open.

[Vincent Beffara]

PR'd at #16489 (together with the uniqueness theorem for analytic functions, which was the motivation for the statement).