Commit 2020-05-12 15:37 ff184e6d

View on Github →

feat(analysis/normed_space): add Mazur-Ulam theorem (#2214) Based on a proof by Jussi Väisälä, see journal version or preprint on web.archive. Also rename reflection to point_reflection as was suggested by @rwbarton and @PatrickMassot

Estimated changes

Modified docs/references.bib

Modified src/algebra/midpoint.lean

added theorem equiv.point_reflection_midpoint_left

added theorem equiv.point_reflection_midpoint_right

deleted theorem equiv.reflection_midpoint_left

deleted theorem equiv.reflection_midpoint_right

Created src/analysis/normed_space/mazur_ulam.lean

added theorem isometric.coe_to_real_linear_equiv_of_map_zero

added theorem isometric.coe_to_real_linear_equiv_of_map_zero_symm

added theorem isometric.map_midpoint

added theorem isometric.midpoint_fixed

added def isometric.to_real_linear_equiv

added theorem isometric.to_real_linear_equiv_apply

added def isometric.to_real_linear_equiv_of_map_zero

added theorem isometric.to_real_linear_equiv_symm_apply

Created src/analysis/normed_space/point_reflection.lean

added theorem equiv.point_reflection_fixed_iff_of_module

added def isometric.point_reflection

added theorem isometric.point_reflection_apply

added theorem isometric.point_reflection_dist_fixed

added theorem isometric.point_reflection_dist_self'

added theorem isometric.point_reflection_dist_self

added theorem isometric.point_reflection_dist_self_real

added theorem isometric.point_reflection_fixed_iff

added theorem isometric.point_reflection_involutive

added theorem isometric.point_reflection_midpoint_left

added theorem isometric.point_reflection_midpoint_right

added theorem isometric.point_reflection_self

added theorem isometric.point_reflection_symm

added theorem isometric.point_reflection_to_equiv

Modified src/analysis/normed_space/real_inner_product.lean

Deleted src/analysis/normed_space/reflection.lean

deleted theorem equiv.reflection_fixed_iff_of_module

deleted def isometric.reflection

deleted theorem isometric.reflection_apply

deleted theorem isometric.reflection_dist_fixed

deleted theorem isometric.reflection_dist_self'

deleted theorem isometric.reflection_dist_self

deleted theorem isometric.reflection_dist_self_real

deleted theorem isometric.reflection_fixed_iff

deleted theorem isometric.reflection_involutive

deleted theorem isometric.reflection_midpoint_left

deleted theorem isometric.reflection_midpoint_right

deleted theorem isometric.reflection_self

deleted theorem isometric.reflection_symm

deleted theorem isometric.reflection_to_equiv

Modified src/data/equiv/mul_add.lean

added def equiv.point_reflection

added theorem equiv.point_reflection_apply

added theorem equiv.point_reflection_fixed_iff_of_bit0_inj

added theorem equiv.point_reflection_involutive

added theorem equiv.point_reflection_self

added theorem equiv.point_reflection_symm

deleted def equiv.reflection

deleted theorem equiv.reflection_apply

deleted theorem equiv.reflection_fixed_iff_of_bit0_inj

deleted theorem equiv.reflection_involutive

deleted theorem equiv.reflection_self

deleted theorem equiv.reflection_symm

Modified src/order/conditionally_complete_lattice.lean

modified theorem cinfi_le

modified theorem le_csupr

Modified src/topology/metric_space/gluing.lean

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/metric_space/isometry.lean

added theorem isometric.add_left_symm

added theorem isometric.add_left_to_equiv

added theorem isometric.add_right_apply

added theorem isometric.add_right_symm

added theorem isometric.add_right_to_equiv

added theorem isometric.coe_add_left

added theorem isometric.coe_add_right

added theorem isometric.coe_neg

added theorem isometric.neg_symm

added theorem isometric.neg_to_equiv

added theorem isometric.symm_symm

added theorem isometric.symm_trans_apply