Commit 2025-04-14 15:20 212d4936
View on Github →fix(CompletelyRegularSpace): fix lemmas (#24017)
Fix some oddities caused by a rogue section variable. For example, separatesPoints_continuous_of_completelyRegularSpace assumes [CompletelyRegularSpace X] [T1Space X], which is just equivalent to [T35Space X].