toRealAffineIsometryEquiv — Mathlib

English

The function underlying the real-affine isometry equivalence equals the action of the isometry on points, preserving the affine structure.

Русский

Функция, лежащая в основе real-affine изометрии, совпадает с действием изометрии на точки и сохраняет аффинную структуру.

LaTeX

$$$f^{\text{toRealAffineIsometryEquiv}}(p) = f(p)$$$

Lean4

/-- **Mazur-Ulam Theorem**: if `f` is an isometric bijection between two normed add-torsors over
normed vector spaces over `ℝ`, then `f` is an affine isometry equivalence. -/
def toRealAffineIsometryEquiv (f : PE ≃ᵢ PF) : PE ≃ᵃⁱ[ℝ] PF :=
  AffineIsometryEquiv.mk' f
    ((vaddConst (Classical.arbitrary PE)).trans <|
        f.trans (vaddConst (f <| Classical.arbitrary PE)).symm).toRealLinearIsometryEquiv
    (Classical.arbitrary PE) fun p => by simp

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