mathlib

ae3d5722 - chore(topology/uniform_space/basic): Make `to_topological_space_inf` and `inf_uniformity` true by definition (#14912)

chore(topology/uniform_space/basic): Make `to_topological_space_inf` and `inf_uniformity` true by definition (#14912) Since the lattice API lets us provide a definition for `inf`, we may as well provide a nice one such that the obvious properties are true by rfl. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>