span_iUnion — Mathlib

English

The supremum of a collection of subspaces equals the span of the union of the collection.

Русский

Супремум множества подпространств равен span объединения этого множества.

LaTeX

$$$\operatorname{sup}_{i} \operatorname{span}(s_i) = \operatorname{span}(\bigcup_i s_i)$$$

Lean4

/-- The supremum of a collection of subspaces is equal to the span of the union of the
collection. -/
theorem span_iUnion {ι} (s : ι → Set (ℙ K V)) : span (⋃ i, s i) = ⨆ i, span (s i) :=
  (@gi K V _ _ _).gc.l_iSup

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