mem_span_range_iff_exists_fun — Mathlib

English

For x in the span of range v, there exists coefficients c: α → R such that ∑ i c i v i = x.

Русский

Для x, принадлежащего span (range v), существует набор коэффициентов c : α → R, таких что ∑ i c i v i = x.

LaTeX

$$$x \\in \\operatorname{span}_R(\\operatorname{range} v) \\iff \\exists c : \\alpha \\to R, \\sum_i c_i \\cdot v_i = x$$$

Lean4

/-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`.
-/
theorem mem_span_range_iff_exists_fun : x ∈ span R (range v) ↔ ∃ c : α → R, ∑ i, c i • v i = x :=
  by
  rw [Finsupp.equivFunOnFinite.surjective.exists]
  simp only [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]
  exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

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