Commit 2023-03-08 14:58 7b1655a1

View on Github →

feat: port Topology.MetricSpace.IsometricSmul (#2675)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/IsometricSMul.lean

added theorem EMetric.preimage_mul_left_ball

added theorem EMetric.preimage_mul_left_closedBall

added theorem EMetric.preimage_mul_right_ball

added theorem EMetric.preimage_mul_right_closedBall

added theorem EMetric.preimage_smul_ball

added theorem EMetric.preimage_smul_closedBall

added theorem EMetric.smul_ball

added theorem EMetric.smul_closedBall

added def IsometryEquiv.constSMul

added theorem IsometryEquiv.constSMul_symm

added def IsometryEquiv.divLeft

added def IsometryEquiv.divRight

added theorem IsometryEquiv.divRight_symm

added def IsometryEquiv.inv

added theorem IsometryEquiv.inv_symm

added def IsometryEquiv.mulLeft

added theorem IsometryEquiv.mulLeft_symm

added def IsometryEquiv.mulRight

added theorem IsometryEquiv.mulRight_symm

added theorem Metric.preimage_mul_left_ball

added theorem Metric.preimage_mul_left_closedBall

added theorem Metric.preimage_mul_right_ball

added theorem Metric.preimage_mul_right_closedBall

added theorem Metric.preimage_smul_ball

added theorem Metric.preimage_smul_closedBall

added theorem Metric.preimage_smul_sphere

added theorem Metric.smul_ball

added theorem Metric.smul_closedBall

added theorem Metric.smul_sphere

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 isometry_inv

added theorem isometry_mul_left

added theorem isometry_mul_right

added theorem isometry_smul

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