linearIndepOn_id_range_iff — Mathlib

English

A linear independence of a family is equivalent to the independence of the family restricted to the range of an injective map.

Русский

Линейная независимость семейства эквивалентна независимости семейства, ограниченного на образ инъективного отображения.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R id (\\\\operatorname{range} f) \\\\iff \\\\mathrm{LinearIndependent}_R f.$$$

Lean4

theorem linearIndepOn_id_range_iff {ι} {f : ι → M} (hf : Injective f) :
    LinearIndepOn R id (range f) ↔ LinearIndependent R f :=
  linearIndepOn_range_iff hf id

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