coe_isometryOfOrthonormal — Mathlib

English

If v is orthonormal and f is a linear isometry, then f ∘ v is orthonormal.

Русский

Если v ортонормирована и f — линейная изометрия, то f ∘ v ортонормирована.

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(v) \\Rightarrow \\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v)$ for a linear isometry $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

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