toAffineIsometryEquiv — Mathlib

English

The constructor mk' yields an affine isometry equivalence from a base map and a linear isometry equivalence, defined by the basepoint relation.

Русский

Конструктор mk' формирует аффинную изометрическую эквивалентность, задаваемую базисной связью и линейной эквивалентностью изометрий.

LaTeX

$$$$ mk'(e,e',p,h) : P_1 \simeq^{\mathrm{AI}} P_2, \quad h(p') : e(p') = e'(p' -_v p) +_v e(p). $$$$

Lean4

/-- Reinterpret a linear isometry equiv as an affine isometry equiv. -/
def toAffineIsometryEquiv : V ≃ᵃⁱ[𝕜] V₂ :=
  { e.toLinearEquiv.toAffineEquiv with norm_map := e.norm_map }

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