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

Modified src/analysis/normed/group/add_torsor.lean

deleted def isometric.const_vadd

deleted def isometric.const_vsub

deleted def isometric.vadd_const

added def isometry_equiv.const_vadd

added def isometry_equiv.const_vsub

added def isometry_equiv.vadd_const

Modified src/analysis/normed/group/basic.lean

deleted theorem isometric.coe_inv

deleted theorem isometric.coe_mul_left

deleted theorem isometric.coe_mul_right

deleted theorem isometric.inv_symm

deleted theorem isometric.inv_to_equiv

deleted theorem isometric.mul_left_symm

deleted theorem isometric.mul_left_to_equiv

deleted theorem isometric.mul_right_apply

deleted theorem isometric.mul_right_symm

deleted theorem isometric.mul_right_to_equiv

added theorem isometry_equiv.coe_inv

added theorem isometry_equiv.coe_mul_left

added theorem isometry_equiv.coe_mul_right

added theorem isometry_equiv.inv_symm

added theorem isometry_equiv.inv_to_equiv

added theorem isometry_equiv.mul_left_symm

added theorem isometry_equiv.mul_left_to_equiv

added theorem isometry_equiv.mul_right_apply

added theorem isometry_equiv.mul_right_symm

added theorem isometry_equiv.mul_right_to_equiv

Modified src/analysis/normed_space/add_torsor.lean

Modified src/analysis/normed_space/affine_isometry.lean

deleted theorem affine_isometry_equiv.coe_to_isometric

added theorem affine_isometry_equiv.coe_to_isometry_equiv

modified def affine_isometry_equiv.to_homeomorph

deleted def affine_isometry_equiv.to_isometric

deleted theorem affine_isometry_equiv.to_isometric_refl

deleted theorem affine_isometry_equiv.to_isometric_symm

added def affine_isometry_equiv.to_isometry_equiv

added theorem affine_isometry_equiv.to_isometry_equiv_refl

added theorem affine_isometry_equiv.to_isometry_equiv_symm

Modified src/analysis/normed_space/linear_isometry.lean

deleted theorem linear_isometry_equiv.coe_to_isometric

added theorem linear_isometry_equiv.coe_to_isometry_equiv

modified def linear_isometry_equiv.to_homeomorph

deleted def linear_isometry_equiv.to_isometric

deleted theorem linear_isometry_equiv.to_isometric_inj

deleted theorem linear_isometry_equiv.to_isometric_injective

deleted theorem linear_isometry_equiv.to_isometric_symm

added def linear_isometry_equiv.to_isometry_equiv

added theorem linear_isometry_equiv.to_isometry_equiv_inj

added theorem linear_isometry_equiv.to_isometry_equiv_injective

added theorem linear_isometry_equiv.to_isometry_equiv_symm

Modified src/analysis/normed_space/mazur_ulam.lean

deleted theorem isometric.coe_fn_to_real_affine_isometry_equiv

deleted theorem isometric.coe_to_real_affine_isometry_equiv

deleted theorem isometric.coe_to_real_linear_equiv_of_map_zero

deleted theorem isometric.coe_to_real_linear_equiv_of_map_zero_symm

deleted theorem isometric.map_midpoint

deleted theorem isometric.midpoint_fixed

deleted def isometric.to_real_affine_isometry_equiv

deleted theorem isometric.to_real_linear_equiv_apply

deleted def isometric.to_real_linear_isometry_equiv

deleted def isometric.to_real_linear_isometry_equiv_of_map_zero

deleted theorem isometric.to_real_linear_isometry_equiv_symm_apply

added theorem isometry_equiv.coe_fn_to_real_affine_isometry_equiv

added theorem isometry_equiv.coe_to_real_affine_isometry_equiv

added theorem isometry_equiv.coe_to_real_linear_equiv_of_map_zero

added theorem isometry_equiv.coe_to_real_linear_equiv_of_map_zero_symm

added theorem isometry_equiv.map_midpoint

added theorem isometry_equiv.midpoint_fixed

added def isometry_equiv.to_real_affine_isometry_equiv

added theorem isometry_equiv.to_real_linear_equiv_apply

added def isometry_equiv.to_real_linear_isometry_equiv

added def isometry_equiv.to_real_linear_isometry_equiv_of_map_zero

added theorem isometry_equiv.to_real_linear_isometry_equiv_symm_apply

Modified src/measure_theory/function/conditional_expectation/basic.lean

Modified src/measure_theory/measure/hausdorff.lean

deleted theorem isometric.hausdorff_measure_image

deleted theorem isometric.hausdorff_measure_preimage

added theorem isometry_equiv.hausdorff_measure_image

added theorem isometry_equiv.hausdorff_measure_preimage

deleted theorem measure_theory.outer_measure.isometric_comap_mk_metric

deleted theorem measure_theory.outer_measure.isometric_map_mk_metric

added theorem measure_theory.outer_measure.isometry_equiv_comap_mk_metric

added theorem measure_theory.outer_measure.isometry_equiv_map_mk_metric

Modified src/topology/continuous_function/compact.lean

deleted def continuous_map.isometric_bounded_of_compact

added def continuous_map.isometry_equiv_bounded_of_compact

deleted theorem continuous_map.linear_isometry_bounded_of_compact_to_isometric

added theorem continuous_map.linear_isometry_bounded_of_compact_to_isometry_equiv

Modified src/topology/metric_space/gromov_hausdorff.lean

deleted theorem Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometric

added theorem Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometry_equiv

Modified src/topology/metric_space/hausdorff_dimension.lean

deleted theorem isometric.dimH_image

deleted theorem isometric.dimH_preimage

deleted theorem isometric.dimH_univ

added theorem isometry_equiv.dimH_image

added theorem isometry_equiv.dimH_preimage

added theorem isometry_equiv.dimH_univ

Modified src/topology/metric_space/isometry.lean

deleted theorem isometric.apply_inv_self

deleted theorem isometric.apply_symm_apply

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.coe_to_homeomorph

deleted theorem isometric.coe_to_homeomorph_symm

deleted theorem isometric.comp_continuous_iff'

deleted theorem isometric.comp_continuous_iff

deleted theorem isometric.comp_continuous_on_iff

deleted theorem isometric.complete_space_iff

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_closed_ball

deleted theorem isometric.image_emetric_ball

deleted theorem isometric.image_emetric_closed_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_closed_ball

deleted theorem isometric.preimage_emetric_ball

deleted theorem isometric.preimage_emetric_closed_ball

deleted theorem isometric.preimage_sphere

deleted theorem isometric.preimage_symm

deleted theorem isometric.range_eq_univ

deleted theorem isometric.self_comp_symm

deleted def isometric.simps.apply

deleted def isometric.simps.symm_apply

deleted theorem isometric.symm_apply_apply

deleted theorem isometric.symm_apply_eq

deleted theorem isometric.symm_comp_self

deleted theorem isometric.symm_symm

deleted theorem isometric.symm_trans_apply

deleted theorem isometric.to_equiv_inj

deleted theorem isometric.trans_apply

deleted structure isometric

deleted def isometry.isometric_on_range

added def isometry.isometry_equiv_on_range

added theorem isometry_equiv.apply_inv_self

added theorem isometry_equiv.apply_symm_apply

added theorem isometry_equiv.coe_eq_to_equiv

added theorem isometry_equiv.coe_mul

added theorem isometry_equiv.coe_one

added theorem isometry_equiv.coe_to_equiv

added theorem isometry_equiv.coe_to_homeomorph

added theorem isometry_equiv.coe_to_homeomorph_symm

added theorem isometry_equiv.comp_continuous_iff'

added theorem isometry_equiv.comp_continuous_iff

added theorem isometry_equiv.comp_continuous_on_iff

added theorem isometry_equiv.complete_space_iff

added theorem isometry_equiv.diam_image

added theorem isometry_equiv.diam_preimage

added theorem isometry_equiv.diam_univ

added theorem isometry_equiv.ediam_image

added theorem isometry_equiv.ediam_preimage

added theorem isometry_equiv.ediam_univ

added theorem isometry_equiv.eq_symm_apply

added theorem isometry_equiv.ext

added theorem isometry_equiv.image_ball

added theorem isometry_equiv.image_closed_ball

added theorem isometry_equiv.image_emetric_ball

added theorem isometry_equiv.image_emetric_closed_ball

added theorem isometry_equiv.image_sphere

added theorem isometry_equiv.image_symm

added theorem isometry_equiv.inv_apply_self

added def isometry_equiv.mk'

added theorem isometry_equiv.mul_apply

added theorem isometry_equiv.preimage_ball

added theorem isometry_equiv.preimage_closed_ball

added theorem isometry_equiv.preimage_emetric_ball

added theorem isometry_equiv.preimage_emetric_closed_ball

added theorem isometry_equiv.preimage_sphere

added theorem isometry_equiv.preimage_symm

added theorem isometry_equiv.range_eq_univ

added theorem isometry_equiv.self_comp_symm

added def isometry_equiv.simps.apply

added def isometry_equiv.simps.symm_apply

added theorem isometry_equiv.symm_apply_apply

added theorem isometry_equiv.symm_apply_eq

added theorem isometry_equiv.symm_comp_self

added theorem isometry_equiv.symm_symm

added theorem isometry_equiv.symm_trans_apply

added theorem isometry_equiv.to_equiv_inj

added theorem isometry_equiv.trans_apply

added structure isometry_equiv