finsupp_linearCombination_repr — Mathlib

English

For any w ⊆ M and any x in span_R w, the finitely supported representation of x via Span.repr R w, followed by converting that representation back to a linear combination using Finsupp.linearCombination, yields x.

Русский

Для любого w ⊆ M и любого x в span_R w представление x через Span.repr R w с конечной опорой, затем преобразование обратно в линейную комбинацию с помощью Finsupp.linearCombination восстанавливают x.

LaTeX

$$$Finsupp.linearCombination\, R\ ((\uparrow) : w \to M)\ (Span.repr\, R\ w\ x) = x$$$

Lean4

@[simp]
theorem finsupp_linearCombination_repr {w : Set M} (x : span R w) :
    Finsupp.linearCombination R ((↑) : w → M) (Span.repr R w x) = x :=
  by
  rw [Span.repr_def]
  exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

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