mathlib3
73540423 - fix(topology/metric_space): free universe (#4072)

Commit

5 years ago

fix(topology/metric_space): free universe (#4072) Removes an unneeded and painful universe restriction

References

Author

PatrickMassot

Parents