span_union — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{span}\left(\bigcup_{i} s_i\right) = \bigvee_i \operatorname{span}(s_i)$$$

Lean4

/-- The supremum of two subspaces is equal to the span of their union. -/
theorem span_union (S T : Set (ℙ K V)) : span (S ∪ T) = span S ⊔ span T :=
  (@gi K V _ _ _).gc.l_sup

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