linearIndependent_restrict — Mathlib

English

If LinearIndepOn R v s holds, then the restricted family (s.restrict v) is linearly independent over R.

Русский

Если LinearIndepOn R v s выполняется, то ограниченная последовательность (s.restrict v) линейно независима над R.

LaTeX

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

Lean4

theorem linearIndependent_restrict (hs : LinearIndepOn R v s) : LinearIndependent R (s.restrict v) :=
  hs

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