Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-09 10:22 9f5099ec

View on Github →

refactor(analysis): add uniform_embedding_comap

Estimated changes

Modified analysis/emetric_space.lean

deleted theorem emetric_space.induced_uniform_embedding

Modified analysis/metric_space.lean

deleted theorem metric_space.induced_uniform_embedding

Modified analysis/real.lean

Modified analysis/topology/uniform_space.lean

added theorem uniform_embedding_comap