vectorSpan_union_of_mem_of_mem — Mathlib

English

The vector span of a union of sets with a common point equals the sum (sup) of their vector spans.

Русский

Вектор Span объединения множеств с общей точкой равен сумме (объединению) их векторных Span.

LaTeX

$$$\\operatorname{vectorSpan}_k(s_1 \\cup s_2) = \\operatorname{vectorSpan}_k(s_1) \\sqcup \\operatorname{vectorSpan}_k(s_2)$$$

Lean4

/-- The vector span of a union of sets with a common point is the sup of their vector spans. -/
theorem vectorSpan_union_of_mem_of_mem {s₁ s₂ : Set P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) :
    vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂ := by
  simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]

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