English
The linear map produced by constrL is the same as the linear map produced by constr; i.e., the linear map underlying v.constrL f equals v.constr 𝕜 f.
Русский
Линейное отображение, получаемое через constrL, совпадает с отображением, получаемым через constr; тождественно связь линейных отображений.
LaTeX
$$$(v\\text{.constrL } f) = (v\\text{.constr } f)\\;\\text{as linear maps}$$$
Lean4
/-- The continuous linear equivalence between a vector space over `𝕜` with a finite basis and
functions from its basis indexing type to `𝕜`. -/
@[simps! apply]
def equivFunL (v : Basis ι 𝕜 E) : E ≃L[𝕜] ι → 𝕜 :=
{
v.equivFun with
continuous_toFun :=
haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis v
v.equivFun.toLinearMap.continuous_of_finiteDimensional
continuous_invFun := by
change Continuous v.equivFun.symm.toFun
exact v.equivFun.symm.toLinearMap.continuous_of_finiteDimensional }
