isometryOfOrthonormal_toLinearEquiv

English

Given an orthonormal basis v in E and an orthonormal basis v' in E', the equivalence hv ≡ hv' e is an isometry between E and E' when mapped along e.

Русский

Пусть дан ортонормированный базис v в E и ортонормированный базис v' в E'; эквивалентность hv hv' e задаёт изометрическое отображение между E и E' через отображение базисов по e.

LaTeX

$$$hv.equiv hv' e: E \\to E'$ is an isometry when $e$ is a bijection between the index sets.$$

Lean4

@[simp]
theorem isometryOfOrthonormal_toLinearEquiv (f : E ≃ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v)
    (hf : Orthonormal 𝕜 (f ∘ v)) : (f.isometryOfOrthonormal hv hf).toLinearEquiv = f :=
  rfl

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