Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-17 03:47 2c4a5161

View on Github →

chore(topology/metric_space/isometry): a few more lemmas (#5780) Also reuse more proofs about inducing and quotient_map in topology/homeomorph. Non-bc change: rename isometric.range_coe to isometric.range_eq_univ to match equiv.range_eq_univ.

Estimated changes