equiv_apply — Mathlib

English

The Pi-basis in Euclidean space is an orthonormal basis mapping i to the unit vector at i.

Русский

База Pi в Евклидовом пространстве образует ортонормированную базу, отправляя индекс i в вектор-единицу на i.

LaTeX

$$$$ \\text{basisFun }\\;\\iota\\;\\mathbb{K} \\; i = \\text{single vector at } i. $$$$

Lean4

theorem equiv_apply (x : E) : b.equiv b' e x = ∑ i, b.repr x i • b' (e i) :=
  by
  nth_rw 1 [← b.sum_repr x, map_sum]
  simp_rw [map_smul, equiv_apply_basis]

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