LinearIndepOn — Mathlib

English

For a subset s ⊆ ι, the vectors of v indexed by s are linearly independent over R.

Русский

Для подмножества s ⊆ ι вектора v, индексируемые по элементам s, линейно независимы над R.

LaTeX

$$$\\operatorname{LinearIndepOn}(R,v,s) \\;:=\\; \\operatorname{LinearIndependent}\\left(R,\\;\\lambda x:s\\to v(x)\\right)$$$

Lean4

/-- `LinearIndepOn R v s` states that the vectors in the family `v` that are indexed
by the elements of `s` are linearly independent over `R`. -/
def LinearIndepOn (s : Set ι) : Prop :=
  LinearIndependent R (fun x : s ↦ v x)

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