Theorem Metric.tendsto_nhdsSet

Modification history

2026-05-19 19:46
Mathlib/Topology/MetricSpace/Thickening.lean
feat(Topology): lemmas about `nhdsSet` filter (#39350)
Added Metric.tendsto_nhdsSetView on Github →