repr_eq_single — Mathlib

English

If a vector x in the span of the v_i equals v_i itself for some i, then its coordinates are given by the single-term coefficient at i, i.e., the representation ivector is the single-term function at i with value 1.

Русский

Если векторы x из пространства, лежащего в порождающем пространстве образа v, совпадает с v_i для некоторого i, то его координаты равны единичному вектору в позиции i.

LaTeX

$$$\uparrow x = v_i \quad\Rightarrow\quad hv.repr x = Finsupp.single i 1$$$

Lean4

theorem repr_eq_single (i) (x : span R (range v)) (hx : ↑x = v i) : hv.repr x = Finsupp.single i 1 :=
  by
  apply hv.repr_eq
  simp [Finsupp.linearCombination_single, hx]

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