id_imageₛ — Mathlib

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)

Похожие утверждения