Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 06:39 ef428c61

View on Github →

feat(topology/metric_space): add uniform_embedding.comap_metric_space (#8838)

  • add uniform_embedding.comap_metric_space and uniform_inducing.comap_pseudo_metric_space;
  • use the former for int.metric_space;
  • also add emetric.closed_ball_mem_nhds.

Estimated changes