instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal

Mathlib.Analysis.InnerProductSpace.l2Space

URI: https://scilib.ai/kg/mathlib#HilbertBasis.instInhabitedSubtypePreLpMemAddSubgroupLpOfNatENNReal

English

For a Hilbert basis, the inverse image on a single basis vector lp.single 2 i x yields V_i x.

Русский

Для гильбертовой базы обратное отображение на один вектор базиса даёт V_i x.

LaTeX

$$$ h_V.linearIsometryEquiv.symm (lp.single 2 i x) = V_i x $$$

Lean4

instance {ι : Type*} : Inhabited (HilbertBasis ι 𝕜 ℓ²(ι, 𝕜)) :=
  ⟨ofRepr (LinearIsometryEquiv.refl 𝕜 _)⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru