Theorem mapClusterPt_atTop_iff_forall_mem_closure

Modification history

2026-03-27 17:46
Mathlib/Topology/ClusterPt.lean
feat(Topology/Compactness): add countably compact sets (#36174) …
Added mapClusterPt_atTop_iff_forall_mem_closureView on Github →