top_le_span_range_iff_forall_exists_fun

English

For s ⊆ α, an element x lies in span of v'' s iff there exists coefficients c : s → R with ∑ c i · v i = x.

Русский

Для множества s ⊆ α элемент x лежит в span(v'' s) тогда, когда существуют коэффициенты c : s → R такие что сумма ∑ 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

/-- A family `v : α → V` is generating `V` iff every element `(x : V)`
can be written as sum `∑ cᵢ • vᵢ = x`.
-/
theorem top_le_span_range_iff_forall_exists_fun : ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, ∑ i, c i • v i = x :=
  by
  simp_rw [← mem_span_range_iff_exists_fun]
  exact ⟨fun h x => h trivial, fun h x _ => h x⟩

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