This is a preliminary formalization of Algebraic Theory of General Topology, possibly yet not compiling. In the future I am going to submit it as a push request to MathLib.
I am going to use it to check my proof of Navier-Stokes Millennium Problem using this formalization.