constr_apply_fintype — Mathlib

English

For finite index types, the constr map expands as a finite sum of basis-weighted images.

Русский

Для конечного индекса сумму линейной комбинации над элементами базиса можно выписать как конечную сумму.

LaTeX

$$$(\\mathrm{constr}\\, b\\ S\\ f)(x) = \\sum_{i \\in ι} (b.\\mathrm{equivFun}\\ x\\ i) \\cdot f(i).$$$

Lean4

@[simp]
theorem constr_apply_fintype [Fintype ι] (b : Basis ι R M) (f : ι → M') (x : M) :
    (constr (M' := M') b S f : M → M') x = ∑ i, b.equivFun x i • f i := by
  simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]

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