Mathlib Changelog
v4
Changelog
About
Github
Theorem
Metric.mem_nhdsSet_iff
Modification history
2026-05-19 19:46
Mathlib/Topology/MetricSpace/Thickening.lean
feat(Topology): lemmas about `nhdsSet` filter (#39350)
Added
Metric.mem_nhdsSet_iff
View on Github →