Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 21:49 b82c0d25

View on Github →

feat(topology/metric_space/isometry): (pre)image of a (closed) ball or a sphere (#10813) Also specialize for translations in a normed add torsor.

Estimated changes

added theorem vadd_ball
added theorem vadd_closed_ball
added theorem vadd_sphere
added theorem isometric.image_ball
added theorem isometric.image_sphere
modified theorem isometry.diam_image
modified theorem isometry.diam_range
added theorem isometry.maps_to_ball
modified theorem isometry.tendsto_nhds_iff