mem_span_image_iff_exists_fun — Mathlib

English

For any s, x ∈ span R (v'' s) iff there exists a finite subset t ⊆ s and coefficients on t giving x.

Русский

Для любого s, x в span R (v'' s) эквивалентно существованию конечного поднабора t ⊆ s и коэффициентов на t, дающих x.

LaTeX

$$$x \\in \\operatorname{span}_R(v'' s) \\iff \\exists t: \\mathrm{Finset}\\;\\alpha, t \\subseteq s \\land \\exists c: t \\to R, \\sum i, c i \\cdot v i = x$$$

Lean4

theorem mem_span_image_iff_exists_fun {s : Set α} :
    x ∈ span R (v '' s) ↔ ∃ t : Finset α, ↑t ⊆ s ∧ ∃ c : t → R, ∑ i, c i • v i = x :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
  · obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h
    refine ⟨l.support, hl, l ∘ (↑), ?_⟩
    rw [← hx]
    exact l.support.sum_coe_sort fun a ↦ l a • v a
  · rw [← hx]
    exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

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