Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 23:40 4b99fe0a

View on Github →

chore(topology/metric_space/isometry): rename isometric to isometry_equiv (#18191) The name for isometric bijections is changed to isometry_equiv, to be consistent with linear_isometry_equiv and affine_isometry_equiv.

Estimated changes

deleted theorem isometric.apply_inv_self
deleted theorem isometric.coe_eq_to_equiv
deleted theorem isometric.coe_mul
deleted theorem isometric.coe_one
deleted theorem isometric.coe_to_equiv
deleted theorem isometric.diam_image
deleted theorem isometric.diam_preimage
deleted theorem isometric.diam_univ
deleted theorem isometric.ediam_image
deleted theorem isometric.ediam_preimage
deleted theorem isometric.ediam_univ
deleted theorem isometric.eq_symm_apply
deleted theorem isometric.ext
deleted theorem isometric.image_ball
deleted theorem isometric.image_sphere
deleted theorem isometric.image_symm
deleted theorem isometric.inv_apply_self
deleted def isometric.mk'
deleted theorem isometric.mul_apply
deleted theorem isometric.preimage_ball
deleted theorem isometric.preimage_sphere
deleted theorem isometric.preimage_symm
deleted theorem isometric.range_eq_univ
deleted theorem isometric.self_comp_symm
deleted theorem isometric.symm_apply_eq
deleted theorem isometric.symm_comp_self
deleted theorem isometric.symm_symm
deleted theorem isometric.to_equiv_inj
deleted theorem isometric.trans_apply
deleted structure isometric
added theorem isometry_equiv.coe_mul
added theorem isometry_equiv.coe_one
added theorem isometry_equiv.ext
added structure isometry_equiv