affineIsometryOfStrictConvexSpace

English

Let f be an isometry between real normed torsors whose codomain is strictly convex. Then f is an affine isometry; in particular, distance-preserving maps need not be surjective, but they must be affine.

Русский

Пусть f — изометрия между реализациями нормированных тorсор над ℝ, причём кодома выпукла. Тогда f является аффинной изометрией; при этом изометрия, сохраняющая расстояния, не обязана быть сюръективной, однако должна быть аффинной.

LaTeX

$$$\forall f:\ PF \to PE,\ \mathrm{Isometry}(f) \Rightarrow f \text{ is an affine isometry } PF \to PE.$$$

Lean4

/-- An isometry of `NormedAddTorsor`s for real normed spaces, strictly convex in the case of the
codomain, is an affine isometry.  Unlike Mazur-Ulam, this does not require the isometry to be
surjective. -/
noncomputable def affineIsometryOfStrictConvexSpace (hi : Isometry f) : PF →ᵃⁱ[ℝ] PE :=
  {
    AffineMap.ofMapMidpoint f
      (fun x y => by
        apply eq_midpoint_of_dist_eq_half
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
        · rw [hi.dist_eq, hi.dist_eq]
          simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul])
      hi.continuous with
    norm_map := fun x => by simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq] }

Похожие утверждения