pi_apply_single — Mathlib

English

If x is concentrated in the i-th component, then pi Q evaluates to Q_i of that component.

Русский

Если вектор x имеет единственную ненулевую компоненту в i-й позиции, то pi Q(x) равняется Q_i(x_i).

LaTeX

$$$ \\pi Q(\\Pi\\text{single}_{i} m) = Q_i(m). $$$

Lean4

theorem pi_apply_single [Fintype ι] [DecidableEq ι] (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (i : ι) (m : Mᵢ i) :
    pi Q (Pi.single i m) = Q i m :=
  by
  rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]
  rw [Pi.single_eq_of_ne hj, map_zero]

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