constr_comp — Mathlib

English

If ι is finite, then (constr b S f)(x) = ∑_{i∈ι} (b.equivFun x i) · f i.

Русский

Если индексный множество ι конечное, то (constr b S f)(x) равно сумме по i∈ι: (b.equivFun x i) · f i.

LaTeX

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

Lean4

@[simp]
theorem constr_comp (f : M' →ₗ[R] M') (v : ι → M') : constr (M' := M') b S (f ∘ v) = f.comp (constr (M' := M') b S v) :=
  b.ext fun i => by simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

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