homOfVector_appTop_coord — Mathlib

English

The coordinate function of homOfVector evaluated at the i-th basis coordinate equals the i-th component of the input vector.

Русский

Координатная функция homOfVector, взятая по i-й базисной координате, даёт i-ую компоненту входного вектора.

LaTeX

$$$$\text{homOfVector}(f,v)\_{{\mathrm{appTop}}}(\text{coord}(S,i)) = v_i.$$$$

Lean4

@[simp]
theorem homOfVector_appTop_coord (i) : (homOfVector f v).appTop (coord S i) = v i := by
  rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly, Equiv.apply_symm_apply]

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