constr_apply — Mathlib

English

For any x ∈ M, (constr b S f)(x) equals the linear combination ∑_i (b.repr x i) • f i.

Русский

Для любого x ∈ M отображение constr b S f применяется как линейная комбинация ∑_i (b.repr x i) • f(i).

LaTeX

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

Lean4

theorem constr_apply (f : ι → M') (x : M) : constr (M' := M') b S f x = (b.repr x).sum fun b a => a • f b :=
  by
  simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]
  rw [Finsupp.sum_mapDomain_index] <;> simp [add_smul]

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