feat: the largest T2 quotient of a topological space.

[PatrickMassot]

trafficstars

---

[PatrickMassot]

Thanks a lot @ADedecker. I was misled by the fact that the T_{2.5} section of the file interrupted the T_2 section. In order to make it easier to review the changes, I used one commit to move things around and then one commit using your simplifications.

[mathlib-bors[bot]]

:v: PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[PatrickMassot]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style