linearIndependent — Mathlib

English

If the subfamily on s is linearly independent, then the restricted map v|s is linearly independent.

Русский

Если подсемейство на s линейно независимо, то ограниченная карта v|s линейно независима.

LaTeX

$$$\\;\\text{If }\\, \\text{LinearIndepOn}(R,v,s)\\text{ then }\\text{LinearIndependent}(R,\\lambda x:s\\to v(x)).$$$

Lean4

theorem linearIndependent {s : Set ι} (h : LinearIndepOn R v s) : LinearIndependent R (fun x : s ↦ v x) :=
  h

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