English
The inverse of the representation map applied to a vector in E equals the image under the basis elements.
Русский
Обратное отображение представления применено к вектору в E даёт образ по элементам базы.
LaTeX
$$$ b.repr.symm(v) = (i \\mapsto \\langle b_i, v \\rangle) $$$
Lean4
/-- `b i` is the `i`th basis vector. -/
instance instFunLike : FunLike (HilbertBasis ι 𝕜 E) ι E
where
coe b i := b.repr.symm (lp.single 2 i (1 : 𝕜))
coe_injective'
| ⟨b₁⟩, ⟨b₂⟩, h => by
congr
apply LinearIsometryEquiv.symm_bijective.injective
apply LinearIsometryEquiv.toContinuousLinearEquiv_injective
apply ContinuousLinearEquiv.coe_injective
refine lp.ext_continuousLinearMap (ENNReal.ofNat_ne_top (n := nat_lit 2)) fun i => ?_
ext
exact congr_fun h i
