mem_span_range_iff_exists_finsupp

English

x ∈ span_R (range v) iff ∃ c : α →₀ R, linearCombination_R (Subtype.val) c = x.

Русский

x принадлежит породжению линейной комбинации диапазона $v$ тогда и только тогда, когда существует $(α→₀R)$-коэффициент $c$ с нужным равенством.

LaTeX

$$$x \\in \\operatorname{span}_R(\\operatorname{range} v) \\iff \\exists c : α →₀ R, \\; \\operatorname{linearCombination}_R(\\operatorname{Subtype.val})\, c = x$$$

Lean4

theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} :
    x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a • v i) = x := by
  simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

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