Theorem IsCompact.inf_nhdsSet_eq_biSup

Modification history

2024-04-03 23:28
Mathlib/Topology/Compactness/Compact.lean
feat: nhdsSet sends intersection of compact sets to their infimum (#11869)
Added IsCompact.inf_nhdsSet_eq_biSupView on Github →