Commit 2025-02-10 19:51 01e44583

chore(Topology/UniformSpace): split into Defs and Basic (#21664) Split Defs.lean off of Basic.lean, including the definition of UniformSpace and UniformContinuous, and all lemmas that can be moved over without increasing imports in Defs.lean. This is motivated by reducing imports for metric spaces, although it seems that EMetricSpace/Defs.lean still needs some results that ended up in Basic.lean. I think the conclusion is that EMetricSpace/Defs.lean should be split further.