constrL_basis — Mathlib

English

For a finite basis v of E and function f: ι → F, the value of the constructed linear map T at the basis vector v_i equals f(i).

Русский

Для конечного базиса v пространства E и отображения f: ι → F значение полученного отображения T на базисном векторе v_i равно f(i).

LaTeX

$$$T := v.constrL f \\implies T(v_i) = f(i) \\text{ for all } i, $ i.e. $(v.constrL f)(v_i) = f(i)$$$

Lean4

@[simp 1100]
theorem constrL_basis (v : Basis ι 𝕜 E) (f : ι → F) (i : ι) : v.constrL f (v i) = f i :=
  v.constr_basis 𝕜 _ _

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