span_iUnion — Mathlib

English

For a family of sets s(i), span of the union equals the supremum of spans: span(⋃i, s(i)) = ⨆ i, span(s(i)).

Русский

Для семейства множеств s(i) покрытие объединения равно наибольшему элементу: span(⋃i, s(i)) = ⨆ i, span(s(i)).

LaTeX

$$$\\operatorname{span}\\Big(\\bigcup_{i} s(i)\\Big) = \\bigvee_{i} \\operatorname{span}(s(i))$$$

Lean4

theorem span_iUnion {ι} (s : ι → Set α) : span (⋃ i, s i) = ⨆ i, span (s i) :=
  Submodule.span_iUnion _

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