coe_isometryOfOrthonormal — Mathlib

English

If hv is an orthonormal basis on E and hf is orthonormal on E under a linear equivalence f, then the corresponding linear equivalence preserves orthonormality.

Русский

Если hv ортонормирован на E, а hf ортонормирован после применения линейной эквивалентности f, то соответствующая линейная эквивалентность сохраняет ортонормированность.

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(v) \\Rightarrow \\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v)$ for a linear equivalence $f$.$$

Lean4

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

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