mathlib3

7dae87fe - feat(topology/metric_space/basic): ext lemmas for metric spaces (#12070)

feat(topology/metric_space/basic): ext lemmas for metric spaces (#12070) Also add a few results in `metric_space.basic`: * A decreasing intersection of closed sets with diameter tending to `0` is nonempty in a complete space * new constructions of metric spaces by pulling back structures (and adjusting definitional equalities) * fixing `metric_space empty` and `metric_space punit` to make sure the uniform structure is definitionally the right one. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>