linearIsometryEquiv — Mathlib

English

A specialized form of IsHilbertSum.mk for actual inclusions from subspaces yields the same conclusion in a convenient form.

Русский

Упрощённая форма IsHilbertSum.mk для реального включения из подпространств даёт тот же вывод в удобной форме.

LaTeX

$$$ IsHilbertSum.mkInternal\\, (F) \\Rightarrow IsHilbertSum 𝕜 G V $$$

Lean4

/-- *A* Hilbert sum `(E, V)` of `G` is canonically isomorphic to *the* Hilbert sum of `G`,
i.e `lp G 2`.

Note that this goes in the opposite direction from `OrthogonalFamily.linearIsometry`. -/
noncomputable def linearIsometryEquiv (hV : IsHilbertSum 𝕜 G V) : E ≃ₗᵢ[𝕜] lp G 2 :=
  LinearIsometryEquiv.symm <| LinearIsometryEquiv.ofSurjective hV.OrthogonalFamily.linearIsometry hV.surjective_isometry

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