English
If hv is a LI family and f is a linear map, then f ∘ v is LI provided appropriate linear structure is respected.
Русский
Если hv образует линейно независимую семью, и f — линейное отображение, то f ∘ v линейно независимо, если соблюдены необходимые условия.
LaTeX
$$$\\text{LinearIndependent } R\\ v \\rightarrow \\forall f:\\ M \\to_{R} M',\\; \\text{Disjoint}(\\operatorname{span} R (\\operatorname{range} v), \\ker f) \\rightarrow \\text{LinearIndependent } R (f \\circ v)$$$
Lean4
/-- If `v` is a linearly independent family of vectors and the kernel of a linear map `f` is
disjoint with the submodule spanned by the vectors of `v`, then `f ∘ v` is a linearly independent
family of vectors. See also `LinearIndependent.map'` for a special case assuming `ker f = ⊥`. -/
theorem map (hv : LinearIndependent R v) {f : M →ₗ[R] M'} (hf_inj : Disjoint (span R (range v)) (LinearMap.ker f)) :
LinearIndependent R (f ∘ v) :=
(f.linearIndependent_iff_of_disjoint hf_inj).mpr hv
