English
If v is LI and v’ is LI, and the spans are disjoint, then Sum.elim v v’ is LI.
Русский
Если v и v’ линейно независимы, и спаны их образов объединены без пересечения, то Sum.elim v v’ линейно независимо.
LaTeX
$$$\\text{LinearIndependent } R\\ v \\,\\to\\, \\text{LinearIndependent } R\\ v' \\,\\to\\, \\text{Disjoint}(\\operatorname{span}R(\\operatorname{range}v), \\operatorname{span}R(\\operatorname{range}v')) \\Rightarrow \\text{LinearIndependent } R\\ (\\mathrm{Sum}.\\mathrm{elim}\\ v\\ v')$$$
Lean4
theorem image {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s)
(hf_inj : Disjoint (span R s) (LinearMap.ker f)) : LinearIndepOn R id (f '' s) :=
hs.id_imageₛ <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj
