mathlib3

581cf19b - feat(topology): split uniform_space and topological_structure