linearIndepOn_id — Mathlib

English

If i is linearly independent, then the image of v on its range is independent, and conversely.

Русский

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

LaTeX

$$$\\\\mathrm{LinearIndependent}_R v \\\\Rightarrow \\\\mathrm{LinearIndepOn}_R id (\\\\operatorname{range} v)$ and equivalently.$$

Lean4

theorem linearIndepOn_id (i : LinearIndependent R v) : LinearIndepOn R id (range v) := by
  simpa using i.comp _ (rangeSplitting_injective v)

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