Commit 2024-04-03 23:28 fcf9a439

View on Github →

feat: nhdsSet sends intersection of compact sets to their infimum (#11869)

Estimated changes

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem IsCompact.inf_nhdsSet_eq_biSup

added theorem IsCompact.mem_inf_nhdsSet_of_forall

added theorem IsCompact.mem_nhdsSet_inf_of_forall

added theorem IsCompact.nhdsSet_inf_eq_biSup

Modified Mathlib/Topology/Separation.lean

added theorem IsCompact.nhdsSet_inter_eq

Modified scripts/style-exceptions.txt