mem_span_image_iff_exists_fun — Mathlib

English

In the finite-index setting, x ∈ span_R (v'' s) iff ∃ c : s → R with ∑ c i · v i = x.

Русский

В конечном случае x ∈ span_R (v'' s) эквивалентно существованию коэффициентов c : s → R such that ∑ c i · v i = x.

LaTeX

$$$x \\in \\operatorname{span}_R (v'' s) \\iff \\exists c : s \\to R, \\sum i, c i \\cdot v i = x$$$

Lean4

theorem mem_span_image_iff_exists_fun {s : Set α} [Fintype s] : x ∈ span R (v '' s) ↔ ∃ c : s → R, ∑ i, c i • v i = x :=
  by rw [← mem_span_range_iff_exists_fun, image_eq_range]

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