linearIsometry — Mathlib

English

If f is an affine isometry between normed affine spaces, then its underlying linear map is a linear isometry; i.e., ∥f.linearIsometry(v)∥ = ∥v∥ for all v.

Русский

Если f является аффинной изометрией между нормированными аффиновыми пространствами, то его связанная линейная часть является линейной изометрией; то есть ∥f.linearIsometry(v)∥ = ∥v∥ для всех v.

LaTeX

$$$\forall v \in V, \ \|f.linearIsometry(v)\| = \|v\|.$$$

Lean4

/-- The underlying linear map of an affine isometry is in fact a linear isometry. -/
protected def linearIsometry : V →ₗᵢ[𝕜] V₂ :=
  { f.linear with norm_map' := f.norm_map }

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