Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 18:27 0b1e039b

View on Github →

feat(topology/metric_space/isometry): use namespace, add lemmas (#15591)

  • Use namespace isometry.
  • Add lemmas like isometry.preimage_ball.

Estimated changes

modified theorem isometry.antilipschitz
modified theorem isometry.closed_embedding
modified theorem isometry.comp
deleted theorem isometry.continuous
deleted theorem isometry.dist_eq
modified theorem isometry.ediam_image
modified theorem isometry.ediam_range
modified theorem isometry.edist_eq
deleted theorem isometry.embedding
deleted theorem isometry.injective
modified theorem isometry.lipschitz
deleted theorem isometry.nndist_eq
added theorem isometry.preimage_ball
modified theorem isometry.right_inv
modified theorem isometry.tendsto_nhds_iff
deleted theorem isometry.uniform_inducing
modified theorem isometry_id
added theorem isometry_iff_dist_eq
added theorem isometry_iff_nndist_eq
modified theorem isometry_subsingleton
modified theorem isometry_subtype_coe