coprodMap_apply — Mathlib

English

For a family f_i of linear maps, applying coprodMap to a single-coordinate input x in M_i yields f_i(x).

Русский

Для семейства линейных отображений f_i применение coprodMap к элементу с одной не нулевой координатой в M_i даёт f_i(x).

LaTeX

$$$coprodMap\\ f\\ (single\\ i\\ x) = f_i\\ x$$$

Lean4

theorem coprodMap_apply [∀ x : N, Decidable (x ≠ 0)] (f : ∀ i : ι, M i →ₗ[R] N) (x : Π₀ i, M i) :
    coprodMap f x = DFinsupp.sum (mapRange (fun i => f i) (fun _ => LinearMap.map_zero _) x) fun _ => id :=
  DFinsupp.sumAddHom_apply _ _

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