span_mul_span — Mathlib

English

The product of the span of S with the span of T equals the span of the product set ST.

Русский

Произведение оболочки множества S на оболочку множества T равно оболочке множества ST.

LaTeX

$$$\\operatorname{span}_R(S) \\cdot \\operatorname{span}_R(T) = \\operatorname{span}_R(S T)$$$

Lean4

theorem span_mul_span : span R S * span R T = span R (S * T) := by rw [mul_eq_map₂]; apply map₂_span_span

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