mathlib

71e37add - Defining an uniform_space by a uniformity basis