Theorem IsCompact.mem_nhdsSet_inf_of_forall

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.mem_nhdsSet_inf_of_forallView on Github →