English
For a linearly independent family v, and any x in the span of range v, the Span representation of x is obtained from hv.repr x by transporting along the injective map from indices to the range of v.
Русский
Для линейно независимого семейства v любой элемент x, принадлежащий span образа v, представляется через Span.repr и hv.repr x переносится по взаимно однозначному соответствию индексов и образа v.
LaTeX
$$$Span.repr R (Set.range v) x = hv.repr x\equivMapDomain (Equiv.ofInjective _ hv.injective)$$$
Lean4
theorem span_repr_eq [Nontrivial R] (x) :
Span.repr R (Set.range v) x = (hv.repr x).equivMapDomain (Equiv.ofInjective _ hv.injective) :=
by
have p : (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm = hv.repr x :=
by
apply (LinearIndependent.linearCombinationEquiv hv).injective
ext
simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
Span.finsupp_linearCombination_repr]
ext ⟨_, ⟨i, rfl⟩⟩
simp [← p]
