linearIndependent_restrict_iff — Mathlib

English

Let s be a subset of ι and v: ι → M. The family {v i : i ∈ s} is linearly independent over R if and only if the family v is linearly independent on s.

Русский

Пусть s ⊆ ι и v: ι → M. Множество {v i : i ∈ s} линейно независимо над R тогда и только тогда, когда семейство v линейно независимо на s.

LaTeX

$$$$ \operatorname{LinearIndependent}_R\left( s \restriction v \right) \iff \operatorname{LinearIndepOn}_R(v,s) \;.$$$$

Lean4

theorem linearIndependent_restrict_iff : LinearIndependent R (s.restrict v) ↔ LinearIndepOn R v s :=
  Iff.rfl

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