English
For a function space, the action of the single-entry function (i ↦ 1, others 0) on x ∈ A is supported only at the i-th coordinate: evaluation matches the i-th coordinate of the function with x.
Русский
В пространстве функций действие единичной функции (i ↦ 1, остальные 0) на x ∈ A действует только в координате i; значение на j равно значению на j для соответствующей функции с x.
LaTeX
$$$\\text{Pi.single\_apply\_smul} \\ (x:\\, A)\\ (i,j:\\, \\iota),\\quad (\\mathrm{Pi.single}\\ i\\ 1:\\, \\iota \\to M_0)\\!\\! j \\cdot x = (\\mathrm{Pi.single}\\ i\\ x:\\, \\iota \\to A)\\! j$$$
Lean4
theorem single_apply_smul {ι : Type*} [DecidableEq ι] (x : A) (i j : ι) :
(Pi.single i 1 : ι → M₀) j • x = (Pi.single i x : ι → A) j := by
rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
