English
If a subset s is linearly independent (with respect to the identity) and a linear map f is injective on the span of s, then the image f''s is linearly independent.
Русский
Если подмножество s линейно независимо (относительно тождества) и линейное отображение f инъективно на подпространстве порождённом s, то образ f '' s линейно независим.
LaTeX
$$$\\text{LinearIndepOn } R\\ id\\ s \\rightarrow \\text{Set.InjOn } f (\\operatorname{span}_R s) \\rightarrow \\text{LinearIndepOn } R\\ id (f''s)$$$
Lean4
theorem id_imageₛ {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s) (hf_inj : Set.InjOn f (span R s)) :
LinearIndepOn R id (f '' s) :=
id_image <| hs.map_injOn f (by simpa using hf_inj)