Commit 2023-09-07 05:43 cdd09f00

View on Github →

feat: add an instance for T3Space (#6861) Add an instance [T0Space α] [RegularSpace α] : T3Space α, drop now unneeded lemmas like TopologicalGroup.t3Space.

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Integrability.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

deleted theorem TopologicalGroup.t2Space

deleted theorem TopologicalGroup.t3Space

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Separation.lean