Commit 2023-09-05 15:17 03c21faf

View on Github →

feat(Topology): add IsCompact.nhdsSet_prod_eq etc (#6961) Also delete NhdsContainBoxes and related lemmas as they were only used for another proof of generalized_tube_lemma.

Estimated changes

Modified Mathlib/Topology/SubsetProperties.lean

added theorem IsCompact.mem_nhdsSet_prod_of_forall

added theorem IsCompact.mem_prod_nhdsSet_of_forall

added theorem IsCompact.nhdsSet_prod_eq

added theorem IsCompact.nhdsSet_prod_eq_biSup

added theorem IsCompact.prod_nhdsSet_eq_biSup

deleted theorem NhdsContainBoxes.comm

deleted theorem NhdsContainBoxes.symm

deleted def NhdsContainBoxes

deleted theorem nhdsContainBoxes_of_compact

deleted theorem nhdsContainBoxes_of_singleton

added theorem nhdsSet_prod_le