coe_constrL — Mathlib

English

If E has a finite basis ι, then E is continuously linearly isomorphic to ι → 𝕜 via the coordinate map given by the basis. This is the canonical coordinate/representation equivalence.

Русский

Если у пространства E есть конечный базис индексный набор ι, то E непрерывно линейно изоморфно пространства функций ι → 𝕜 через координатный отображатель, задаваемый базисом.

LaTeX

$$$E \\simeq_L[𝕜] (ι \\to 𝕜)$$$

Lean4

@[simp]
theorem coe_constrL (v : Basis ι 𝕜 E) (f : ι → F) : (v.constrL f : E →ₗ[𝕜] F) = v.constr 𝕜 f :=
  rfl

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