Theorem Metric.nhds_basis_closedBall_inv_nat_pos

Modification history

2026-02-18 18:21
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
feat: neighborhood basis in a metric space consisting of closed balls of radius `1 / (n + 1)` (#35207)
Added Metric.nhds_basis_closedBall_inv_nat_posView on Github →