span_union — Mathlib

English

The span of a union equals the supremum of the spans of the pieces.

Русский

Объединение порождаемых множеств имеет оболочку, равную наибольшему верхнему пределу порождаемых частях.

LaTeX

$$$\\mathrm{affineSpan}(k, s \\cup t) = \\mathrm{affineSpan}(k,s) \\vee \\mathrm{affineSpan}(k,t)$$$

Lean4

/-- The span of a union of sets is the sup of their spans. -/
theorem span_union (s t : Set P) : affineSpan k (s ∪ t) = affineSpan k s ⊔ affineSpan k t :=
  (AffineSubspace.gi k V P).gc.l_sup

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