English
There is a bi-implication between membership in span generated by the image and the corresponding support condition of coordinates under the basis.
Русский
Существуют двусторонние эквивалентности между принадлежностью span от образа и условием поддержки координат.
LaTeX
$$$(m)\in \operatorname{span}\big(\operatorname{image}(b,s)\big) \iff \text{support}(b^{-1}(m)) \subseteq s.$$$
Lean4
theorem mem_span_image {m : M} {s : Set ι} : m ∈ span R (b '' s) ↔ ↑(b.repr m).support ⊆ s :=
⟨repr_support_subset_of_mem_span _ _, fun h ↦ span_mono (Set.image_mono h) (mem_span_repr_support b _)⟩