Commit 2024-12-18 10:57 2375546c

chore(Topology/Separation): split large file (#20031) This splits up the behemoth Mathlib.Topology.Separation.Basic (2700 lines) into 5 smaller files:

• Mathlib.Topology.Separation.SeparatedNhds: auxiliary definitions of SeparatedNhds and HasSeparatingCover
• Mathlib.Topology.Separation.Basic: T0, R0, T1 and R1 spaces
• Mathlib.Topology.Separation.Hausdorff: T2 and T2.5 spaces
• Mathlib.Topology.Separation.Regular: regular, normal, completely normal, T3-T5
• Mathlib.Topology.Separation.Profinite: totally disconnected compact Hausdorff spaces are totally separated. It also moves Mathlib.Topology.CompletelyRegular and Mathlib.Topology.CountableSeparatingOn into the Separation directory. The only changes outside the files listed above are updating import lines. The only change to actual code is in Mathlib.Topology.Separation.Profinite, where I realised that we had two theorems asserting exactly the same thing, one under strictly more general typeclass hypotheses than the other (locally compact rather than compact spaces). So I made the less general theorem into a deprecated alias for the more general one.