Theorem IsCompact.tendsto_nhdsSet_of_mapClusterPt

Modification history

2026-05-19 19:46
Mathlib/Topology/Compactness/Compact.lean
feat(Topology): lemmas about `nhdsSet` filter (#39350)
Added IsCompact.tendsto_nhdsSet_of_mapClusterPtView on Github →