Commit 2023-01-31 21:08 832a8ba8

View on Github →

feat(topology/metric_space/isometric_smul): new file (#18130) Define typeclasses has_isometric_smul and has_isometric_vadd. To minimize diff size, I did not fully deduplicate lemmas in this PR.

Estimated changes

Modified src/analysis/complex/upper_half_plane/metric.lean

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

modified theorem dist_vadd_cancel_left

deleted def isometry_equiv.const_vadd

deleted theorem vadd_ball

deleted theorem vadd_closed_ball

deleted theorem vadd_sphere

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

deleted theorem dist_div_left

deleted theorem dist_div_right

deleted theorem dist_inv_inv

deleted theorem dist_mul_left

deleted theorem dist_mul_right

deleted theorem edist_div_left

deleted theorem edist_div_right

deleted theorem edist_inv

deleted theorem edist_inv_inv

deleted theorem edist_mul_left

deleted theorem edist_mul_right

deleted theorem isometry_equiv.coe_inv

deleted theorem isometry_equiv.coe_mul_left

deleted theorem isometry_equiv.coe_mul_right

deleted theorem isometry_equiv.inv_symm

deleted theorem isometry_equiv.inv_to_equiv

deleted theorem isometry_equiv.mul_left_symm

deleted theorem isometry_equiv.mul_left_to_equiv

deleted theorem isometry_equiv.mul_right_apply

deleted theorem isometry_equiv.mul_right_symm

deleted theorem isometry_equiv.mul_right_to_equiv

Modified src/analysis/normed_space/basic.lean

deleted theorem dist_smul

added theorem dist_smul₀

deleted theorem nndist_smul

added theorem nndist_smul₀

Modified src/analysis/normed_space/pointwise.lean

Modified src/analysis/seminorm.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

Created src/topology/metric_space/isometric_smul.lean

added theorem dist_div_left

added theorem dist_div_right

added theorem dist_inv_inv

added theorem dist_mul_left

added theorem dist_mul_right

added theorem dist_smul

added theorem edist_div_left

added theorem edist_div_right

added theorem edist_inv

added theorem edist_inv_inv

added theorem edist_mul_left

added theorem edist_mul_right

added theorem edist_smul_left

added theorem emetric.preimage_mul_left_ball

added theorem emetric.preimage_mul_left_closed_ball

added theorem emetric.preimage_mul_right_ball

added theorem emetric.preimage_mul_right_closed_ball

added theorem emetric.preimage_smul_ball

added theorem emetric.preimage_smul_closed_ball

added theorem emetric.smul_ball

added theorem emetric.smul_closed_ball

added def isometry_equiv.const_smul

added theorem isometry_equiv.const_smul_symm

added def isometry_equiv.div_left

added def isometry_equiv.div_right

added theorem isometry_equiv.div_right_symm

added def isometry_equiv.inv

added theorem isometry_equiv.inv_symm

added def isometry_equiv.mul_left

added theorem isometry_equiv.mul_left_symm

added def isometry_equiv.mul_right

added theorem isometry_equiv.mul_right_symm

added theorem isometry_inv

added theorem isometry_mul_left

added theorem isometry_mul_right

added theorem metric.preimage_mul_left_ball

added theorem metric.preimage_mul_left_closed_ball

added theorem metric.preimage_mul_right_ball

added theorem metric.preimage_mul_right_closed_ball

added theorem metric.preimage_smul_ball

added theorem metric.preimage_smul_closed_ball

added theorem metric.preimage_smul_sphere

added theorem metric.smul_ball

added theorem metric.smul_closed_ball

added theorem metric.smul_sphere

added theorem nndist_div_left

added theorem nndist_div_right

added theorem nndist_inv_inv

added theorem nndist_mul_left

added theorem nndist_mul_right

added theorem nndist_smul

Modified src/topology/metric_space/isometry.lean

added theorem isometry.prod_map

added theorem isometry_dcomp