Commit 2025-10-27 04:03 cd0d3577

View on Github →

feat(Topology/UniformSpace/OfCompactT2): generalize theorem (#30917) This PR continues the work from #24103. Original PR: https://github.com/leanprover-community/mathlib4/pull/24103

Estimated changes

Modified Mathlib/Topology/Separation/Regular.lean

added theorem disjoint_nested_nhds_of_not_inseparable

Modified Mathlib/Topology/UniformSpace/OfCompactT2.lean

added def uniformSpaceOfCompactR1

deleted def uniformSpaceOfCompactT2

Modified scripts/noshake.json