English
The function underlying Finsupp.basis is precisely the map sending g to the family of singletons built from g’s components.
Русский
Функция, лежащая в основании Finsupp.basis, равна отображению g в семействo единичных базисных векторов, собранных по компонентам g.
LaTeX
$$$\\bigl(\\mathrm{Finsupp.basis}\\; b\\bigr) = \\lambda \\; g. \\lambda i. \\mathrm{single}_{i.1}(b_{i.1}(g_{i.1}))\\,,$$$
Lean4
@[simp]
theorem coe_basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) :
⇑(Finsupp.basis b) = fun ix : Σ i, φ i => single ix.1 (b ix.1 ix.2) :=
funext fun ⟨i, x⟩ =>
Basis.apply_eq_iff.mpr <| by
ext ⟨j, y⟩
by_cases h : i = j
· cases h
simp [Finsupp.single_apply_left sigma_mk_injective]
· simp_all
