coord_equivFun_symm — Mathlib

English

For a finite index set, the i-th coordinate of the Symm-representation of f equals f i: b.coord i (b.equivFun.symm f) = f i.

Русский

Для конечного множества индексов координата i от представления через эквивенная отображение обратно равна f i: b.coord i (b.equivFun.symm f) = f i.

LaTeX

$$$ b.coord\,i (b.equivFun.symm\ f) = f(i) $$$

Lean4

theorem coord_equivFun_symm [Finite ι] (b : Basis ι R M) (i : ι) (f : ι → R) : b.coord i (b.equivFun.symm f) = f i :=
  b.coord_repr_symm i (Finsupp.equivFunOnFinite.symm f)

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