English
Mazur-Ulam: every isometric bijection between real-normed vector spaces yields an associated real-affine isometry equivalence. In particular, an isometry f: E → F gives a real-affine isometry equivalence between E and F.
Русский
Мазур-Улама: любая биекция-изометрия между нормированными по Реалу вековыми пространствами порождает действительную аффинную изометрию. То есть изометрия f: E → F порождает аффинную изометрию между E и F.
LaTeX
$$$f: E \to F$ изометрия ⇒ f\text{ векторная аффинная изометрия } E \simeq_{\mathbb{R}} F$$$
Lean4
/-- A bijective isometry sends midpoints to midpoints. -/
theorem map_midpoint (f : PE ≃ᵢ PF) (x y : PE) : f (midpoint ℝ x y) = midpoint ℝ (f x) (f y) :=
by
set e : PE ≃ᵢ PE :=
((f.trans <| (pointReflection ℝ <| midpoint ℝ (f x) (f y)).toIsometryEquiv).trans f.symm).trans
(pointReflection ℝ <| midpoint ℝ x y).toIsometryEquiv
have hx : e x = x := by simp [e]
have hy : e y = y := by simp [e]
have hm := e.midpoint_fixed hx hy
simp only [e, trans_apply] at hm
rwa [← eq_symm_apply, ← toIsometryEquiv_symm, pointReflection_symm, coe_toIsometryEquiv, coe_toIsometryEquiv,
pointReflection_self, symm_apply_eq, @pointReflection_fixed_iff] at hm
