mem_span_image — Mathlib

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 _)⟩

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