Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-06 00:50 4f7835eb

View on Github →

feat(analysis): add default setup for uniform space of metric space

Estimated changes

Modified analysis/metric_space.lean

added def metric_space.uniform_space_of_dist