dualBasis_coord_toDualEquiv_apply

English

For finite index set, the i-th coordinate of b.toDualEquiv f applied to i equals the i-th coordinate of f with respect to the basis, i.e., b.dualBasis.coord i (b.toDualEquiv f) = b.coord i f.

Русский

Пусть ι конечен. Тогда i-я координата b.toDualEquiv(f) по двойственной базе равна i-й координате f по базису: b.dualBasis.coord i (b.toDualEquiv f) = b.coord i f.

LaTeX

$$$ b.dualBasis.coord i (b.toDualEquiv f) = b.coord i f $$$

Lean4

theorem dualBasis_coord_toDualEquiv_apply [Finite ι] (i : ι) (f : M) :
    b.dualBasis.coord i (b.toDualEquiv f) = b.coord i f := by simp [-toDualEquiv_apply, Basis.dualBasis]

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