of_comp — Mathlib

English

If the image of a family under a linear map is linearly independent, then the original family is linearly independent.

Русский

Если образ семейства вектора под линейным отображением линейно независим, то исходное семейство также линейно независимо.

LaTeX

$$$\\\\mathrm{LinearIndependent}_R (f \\\\circ v) \\\\Rightarrow \\\\mathrm{LinearIndependent}_R v.$$$

Lean4

/-- If the image of a family of vectors under a linear map is linearly independent, then so is
the original family. -/
theorem of_comp (f : M →ₗ[R] M') (hfv : LinearIndependent R (f ∘ v)) : LinearIndependent R v :=
  by
  rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv
  exact hfv.of_comp

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