English
If hv is linearly independent and f is an injection on the image, then the induced map on the index set preserves linear independence after composing with the embedding.
Русский
Если hv линейно независимо и f инъекция на образе, тогда композиция с вложением сохраняет линейную независимость на новом наборе индексов.
LaTeX
$$$\text{LinearIndepOn}_R v s \Rightarrow \text{LinearIndepOn}_R (f \circ v) s$$$
Lean4
/-- If a linear map is injective on the span of a family of linearly independent vectors, then
the family stays linearly independent after composing with the linear map.
See `LinearIndependent.map` for the version with `Set.InjOn` replaced by `Disjoint`
when working over a ring. -/
theorem map_injOn (hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (Set.range v))) :
LinearIndependent R (f ∘ v) :=
(f.linearIndependent_iff_of_injOn hf_inj).mpr hv
