is_open {a} from finite balls

Stream: Is there code for X?

[Xavier Roblot]

Is this result (or something similar) in mathlib? The proof is not very difficult but it might exists already.

example {α : Type*} [metric_space α] (a : α) (h : ∀ r : ℝ, (metric.ball a r).finite) :
  is_open ({a} : set α) :=

[Anatole Dedecker]

docs#infinite_of_mem_nhds seems related but not quite there yet

[Anatole Dedecker]

Actually the proof of docs#infinite_of_mem_nhds is exactly what we want, we just have to remove the extra negation

[Anatole Dedecker]

I suggest replacing the current proof by this, which gives you what you want:

lemma is_open_singleton_iff {α : Type*} [topological_space α] (a : α) :
  is_open ({a} : set α) ↔ (𝓝[≠] a) = ⊥ :=
by rw [is_open_singleton_iff_nhds_eq_pure, nhds_within, ← mem_iff_inf_principal_compl,
        ← le_pure_iff, nhds_ne_bot.le_pure_iff]

lemma is_open_singleton_of_finite_mem_nhds {α : Type*} [topological_space α] [t1_space α]
  (x : α) {s : set α} (hs : s ∈ 𝓝 x) (hsf : s.finite) : is_open ({x} : set α) :=
begin
  have A : {x} ⊆ s, by simp only [singleton_subset_iff, mem_of_mem_nhds hs],
  have B : is_closed (s \ {x}) := (hsf.subset (diff_subset _ _)).is_closed,
  have C : (s \ {x})ᶜ ∈ 𝓝 x, from B.is_open_compl.mem_nhds (λ h, h.2 rfl),
  have D : {x} ∈ 𝓝 x, by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C,
  rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_is_open] at D
end

lemma infinite_of_mem_nhds {α} [topological_space α] [t1_space α] (x : α) [hx : ne_bot (𝓝[≠] x)]
  {s : set α} (hs : s ∈ 𝓝 x) : set.infinite s :=
begin
  refine λ hsf, hx.1 _,
  rw [← is_open_singleton_iff],
  exact is_open_singleton_of_finite_mem_nhds x hs hsf
end

[Xavier Roblot]

Well, that would be great! Can you PR that?

[Anatole Dedecker]

Sure, once I'm done with fighting with the linter in mathlib4 :sweat_smile:

[Xavier Roblot]

Thanks a lot :+1: