apply_single — Mathlib

English

The linear map single i: φ_i → φ_i embedded into the product (i ∈ ι) acts by sending x to the i-th coordinate equal to x and all other coordinates zero.

Русский

Линейное отображение single i: φ_i → ∏_{j∈ι} φ_j отправляет x в такую функцию, что на координате i стоит x, а на остальных координатах ноль.

LaTeX

$$$\\text{single}_i(x)(j)=\\begin{cases} x & j=i, \\\\ 0 & j\\neq i.\\end{cases}$$$

Lean4

theorem apply_single [AddCommMonoid M] [Module R M] [DecidableEq ι] (f : (i : ι) → φ i →ₗ[R] M) (i j : ι) (x : φ i) :
    f j (Pi.single i x j) = (Pi.single i (f i x) : ι → M) j :=
  Pi.apply_single (fun i => f i) (fun i => (f i).map_zero) _ _ _

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