linearIndependent_set_coe_iff — Mathlib

English

The linear independence of a set of elements is equivalent to the linear independence of the corresponding set-indexed family.

Русский

Линейная независимость набора элементов эквивалентна линейной независимости соответствующего семейства, индексируемого этим набором.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\iff \\operatorname{LinearIndepOn}(R,v,s)$ where $s$ ranges over subsets indexing the same family$$

Lean4

theorem linearIndependent_set_coe_iff : LinearIndependent R (fun x : s ↦ v x) ↔ LinearIndepOn R v s :=
  Iff.rfl

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