linearIndepOn_iff_disjoint — Mathlib

English

A non-LI on s is equivalent to the existence of a finitely supported function f such that the sum of f(i) v(i) equals zero, with f supported in s and f nonzero.

Русский

Не-LI на s эквивалентно существованию конечноподдерживаемой функции f, для которой сумма f(i) v(i) равна нулю, причём f поддержано в s и ненулевой.

LaTeX

$$$$\\neg\\operatorname{LinearIndepOn}_R(v,s) \\iff \\exists f : ι \\to R,\\; f \\in \\mathrm{Finsupp.supported}\\,R\\,R\\,s \\wedge \\sum_{i\\in s} f(i)\\,v(i) = 0 \\wedge f \\neq 0.$$$$

Lean4

theorem linearIndepOn_iff_disjoint :
    LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker <| Finsupp.linearCombination R v) := by
  rw [linearIndepOn_iff, LinearMap.disjoint_ker]

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