linearCombination_eq_fintype_linearCombination_apply

English

Another articulation of the finite-index equivalence between linearCombination and its Finite variant.

Русский

Ещё одно формальное выражение эквивалентности для конечного индекса между linearCombination и его конечным вариантом.

LaTeX

$$$\\operatorname{linearCombination}_R v \\circ (Fintype.linearEquivFunOnFinite_R_R \\alpha)^{-1} = Fintype.linearCombination_R v$$$

Lean4

theorem linearCombination_eq_fintype_linearCombination_apply (x : α → R) :
    linearCombination R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) = Fintype.linearCombination R v x :=
  by
  apply Finset.sum_subset
  · exact Finset.subset_univ _
  · intro x _ hx
    rw [Finsupp.notMem_support_iff.mp hx]
    exact zero_smul _ _

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