span_iUnion — Mathlib

English

The span of an indexed union equals the supremum of the spans indexed.

Русский

Оболочка индексированного объединения равна наибольшему верхнему пределу оболочек по индексу.

LaTeX

$$$\\mathrm{affineSpan}(k, \\bigcup_{i} s_i) = \\bigvee_{i} \\mathrm{affineSpan}(k, s_i)$$$

Lean4

/-- The span of a union of an indexed family of sets is the sup of their spans. -/
theorem span_iUnion {ι : Type*} (s : ι → Set P) : affineSpan k (⋃ i, s i) = ⨆ i, affineSpan k (s i) :=
  (AffineSubspace.gi k V P).gc.l_iSup

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