linearIndependent_comp_subtype_iff

English

A standard Finset-based equivalence: LinearIndependent R v is equivalent to the property that if two coefficient functions agree on a Finset, their induced sums agree, hence coefficients must agree on that Finset.

Русский

Стандартное эквивалентность через Finset: LinearIndependent R v эквивалентна свойству, что если две функции коэффициентов совпадают на Finset, то суммы совпадают, следовательно коэффициенты совпадают на этом Finset.

LaTeX

$$$\\operatorname{LinearIndependent}(R,v) \\iff \\forall s:\\operatorname{Finset} ι,\\; \\forall f,g:ι\\to R,\\; (\\sum_{i\\in s} f_i v_i)=(\\sum_{i\\in s} g_i v_i) \\Rightarrow (\\forall i\\in s, f_i=g_i)$$$

Lean4

theorem linearIndependent_comp_subtype_iff : LinearIndependent R (v ∘ Subtype.val : s → M) ↔ LinearIndepOn R v s :=
  Iff.rfl

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