linearIndepOn_iff_image — Mathlib

English

Independence is preserved under applying a linear map to the whole family, i.e., if the image is independent, so is the original family.

Русский

Независимость сохраняется при применении линейного отображения к всему семейству: если образ независим, то и исходное множество независим.

LaTeX

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

Lean4

theorem linearIndepOn_iff_image {ι} {s : Set ι} {f : ι → M} (hf : Set.InjOn f s) :
    LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s) :=
  linearIndependent_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

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