Commit 2026-05-19 19:46 6c16dd93

View on Github →

feat(Topology): lemmas about nhdsSet filter (#39350)

Estimated changes

Modified Mathlib/Order/Filter/Tendsto.lean

added theorem Filter.tendsto_bot_right_iff

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem IsCompact.le_nhdsSet_of_clusterPt

added theorem IsCompact.tendsto_nhdsSet_of_mapClusterPt

Modified Mathlib/Topology/MetricSpace/Thickening.lean

added theorem Metric.mem_nhdsSet_iff

added theorem Metric.tendsto_nhdsSet

modified theorem Metric.thickening_ball

Modified Mathlib/Topology/NhdsSet.lean

added theorem tendsto_nhdsSet_of_tendsto_nhds