prod_span_singleton — Mathlib

English

The product-span of singleton spans equals the span of the product.

Русский

Произведение поодиноких замещений равно замыканию произведения.

LaTeX

$$$\big(\prod_{i\in s} \mathrm{span} (\{x_i\})\big) = \mathrm{span}(\{\prod_{i\in s} x_i\})$$$

Lean4

theorem prod_span_singleton {ι : Type*} (s : Finset ι) (x : ι → A) :
    (∏ i ∈ s, span R ({x i} : Set A)) = span R {∏ i ∈ s, x i} := by rw [prod_span, Set.finset_prod_singleton]

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