Nontrivial closed balls are a basis

Stream: Is there code for X?

[Geoffrey Irving]

Is there the lemma that closedBall x r for r > 0 forms a basis for nhds x?

[Geoffrey Irving]

(This is trivial, and I've already proved it, but I want to confirm that I shouldn't upstream it.)

[Geoffrey Irving]

Ah, found it: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/MetricSpace/Basic.html#Metric.nhds_basis_closedBall

[Eric Wieser]

For future reference, loogle can help here:

[Eric Wieser]

@loogle Filter.HasBasis, Metric.closedBall

[loogle]

:search: Metric.hasBasis_cobounded_compl_closedBall, Metric.nhds_basis_closedBall, and 2 more