coe_basisOfOrthonormalOfCardEqFinrank

English

Let v be an indexed family in E that is orthonormal, and f: E →ₗᵢ[𝕜] E' be a linear isometry. Then the composed family f ∘ v is orthonormal in E' if and only if v is orthonormal in E.

Русский

Пусть v — ортонормированная последовательность в E, а f: E →ₗᵢ[𝕜] E' — линейная изометрия. Тогда последовательность f ∘ v ортонормирована в E' тогда и только тогда, когда v ортонормирована в E.

LaTeX

$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(f \\circ v) \\;\\Leftrightarrow\\; \\operatorname{Orthonormal}_{\\mathbb{K}}(v),$ где $f$ — линейная изометрия.$$

Lean4

@[simp]
theorem coe_basisOfOrthonormalOfCardEqFinrank [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v)
    (card_eq : Fintype.card ι = finrank 𝕜 E) : (basisOfOrthonormalOfCardEqFinrank hv card_eq : ι → E) = v :=
  coe_basisOfLinearIndependentOfCardEqFinrank _ _

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