English
Let B be a basis of a module M indexed by a finite set ι. The coordinate isomorphism b.equivFun : M → (ι → R) coincides with the coordinate representation b.repr : M → (ι → R); hence for every vector u ∈ M, b.equivFun(u) = b.repr(u).
Русский
Пусть B — база модуля M, индексированная скольким-то конечным множеством ι. Изоморфизм координат b.equivFun : M → (ι → R) совпадает с координатным представлением b.repr : M → (ι → R); следовательно для любого вектора u ∈ M выполняется b.equivFun(u) = b.repr(u).
LaTeX
$$$$ \forall ι\; [Finite\, ι]\; (b : Basis\, ι\, R\, M)\; (u : M),\ b.equivFun\, u = b.repr\, u $$$$
Lean4
@[simp]
theorem equivFun_apply [Finite ι] (b : Basis ι R M) (u : M) : b.equivFun u = b.repr u :=
rfl
