vectorSpan_vadd — Mathlib

English

Vector span is invariant under translation: vectorSpan k (v +ᵥ s) = vectorSpan k s.

Русский

Векторное пространство порожденное векторной линейной комбинацией сохраняется при переносе, т.е. vectorSpan k (v +ᵥ s) = vectorSpan k s.

LaTeX

$$$\operatorname{vectorSpan}(k, v +\!\!v s) = \operatorname{vectorSpan}(k, s)$$$

Lean4

@[simp]
theorem vectorSpan_vadd (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s := by simp [vectorSpan]

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