repr_support_subset_of_mem_span — Mathlib

English

For a basis b and a vector m, membership of m in span(b''s) is equivalent to the constraint that the coordinates of m under the basis lie in s.

Русский

Для базиса b и вектора m принадлежность m к span(b''s) эквивалентна тому, что координаты m по базису принадлежат s.

LaTeX

$$$m\in \operatorname{span}\!\big(\operatorname{image}(b\,s)\big) \iff \big( (b.repr\,m).\operatorname{support} \subseteq s \big).$$$

Lean4

theorem repr_support_subset_of_mem_span (s : Set ι) {m : M} (hm : m ∈ span R (b '' s)) : ↑(b.repr m).support ⊆ s :=
  by
  rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩
  rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

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