English
Let I be a finite index set and R a (non-associative) semiring. For any function x: I → R, x is the finite sum of its coordinates against the canonical basis, i.e., x = sum_{i∈I} x(i) e_i, where e_i is the function that is 1 at i and 0 elsewhere.
Русский
Пусть I — конечный индексный набор, R — полугруппа с умножением, и x: I → R. Тогда x представимо как конечная линейная комбинация базисных функций: x = ∑_{i∈I} x(i) e_i, где e_i(j) = 1 если j = i, и 0 иначе.
LaTeX
$$$$ x = \\sum_{i \\in \\mathcal{I}} x(i) \\, e_i, \\quad e_i(j) = \\begin{cases}1 & j=i \\\\ 0 & j\\neq i\\end{cases} $$$$
Lean4
/-- Decomposing `x : ι → R` as a sum along the canonical basis `Pi.single i 1` for `i : ι`. -/
theorem pi_eq_sum_univ' {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [NonAssocSemiring R] (x : ι → R) :
x = ∑ i, (x i) • Pi.single (M := fun _ ↦ R) i 1 :=
by
convert pi_eq_sum_univ x
aesop
