mem_span_image_iff_linearCombination

English

x ∈ span_R (v '' s) iff ∃ l ∈ supported R R s such that linearCombination_R v l = x.

Русский

x принадлежит образу изображения $v''s$ тогда и только тогда, когда существует $l$ с поддержкой в $s$, для которого выполняется линейная комбинация.

LaTeX

$$$x \in \operatorname{span}_R(\operatorname{image} v\; s) \iff \exists l \in \operatorname{supported}_R R s, \; \operatorname{linearCombination}_R v l = x$$$

Lean4

theorem mem_span_image_iff_linearCombination {s : Set α} {x : M} :
    x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, linearCombination R v l = x :=
  by
  rw [span_image_eq_map_linearCombination]
  simp

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