Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsCompact.mem_inf_nhdsSet_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_inf_nhdsSet_of_forall
View on Github →