Singleton is union of nested intervals

Stream: Is there code for X?

[Michael Rothgang]

Is this a slightly unorthodox request: I have a lemma - I'm wondering if mathlib has it, and more important, where it would belong.

import Mathlib
open Set
lemma singleton_eq_inter_Ioo (b : ℝ): {b} = ⋂ (r > 0), Icc (b - r) (b + r) := by
  apply Subset.antisymm
  · simp only [gt_iff_lt, subset_iInter_iff, singleton_subset_iff, mem_Icc, tsub_le_iff_right,
      le_add_iff_nonneg_right, and_self]
    exact fun i hi ↦ hi.le
  · intro x hx
    simp only [gt_iff_lt, mem_iInter, mem_Icc, tsub_le_iff_right] at hx
    simp only [mem_singleton_iff]
    apply le_antisymm
    · exact le_of_forall_pos_le_add (fun r hr ↦ (hx r hr).2)
    · exact le_of_forall_pos_le_add (fun r hr ↦ (hx r hr).1)

#find_home gave me wildly different answers, including Data.Real.Basic (which works, but where it doesn't fit in). Doing so on the playground yields five options; can one of the more seasoned people suggest if any of these is in fact reasonable?

 [Mathlib.Analysis.NormedSpace.HomeomorphBall, Mathlib.Analysis.Normed.Order.UpperLower, Mathlib.Analysis.RCLike.Basic, Mathlib.Analysis.Normed.Group.Quotient, Mathlib.Analysis.Seminorm]

[Richard Osborn]

Should be true for any complete metric space. docs#IsComplete.nonempty_iInter_of_nonempty_biInter seems relevant.

[Alex J. Best]

Heres a proof via the fact that closed balls are a basis

import Mathlib
open Set


lemma singleton_eq_inter_Ioo (b : ℝ): {b} = ⋂ (r > 0), Icc (b - r) (b + r) := by
  simp [Real.Icc_eq_closedBall]
  rw [biInter_basis_nhds Metric.nhds_basis_closedBall]