vectorSpan_empty — Mathlib

English

The vectorSpan of the empty set is the zero subspace ⊥.

Русский

VectorSpan пустого множества равен нуль-подпространству ⊥.

LaTeX

$$$ \\operatorname{vectorSpan} \\ k\\ (\\emptyset : Set P) = (\\bot : Submodule k V) $$$

Lean4

/-- The `vectorSpan` of the empty set is `⊥`. -/
@[simp]
theorem vectorSpan_empty : vectorSpan k (∅ : Set P) = (⊥ : Submodule k V) := by
  rw [vectorSpan_def, vsub_empty, Submodule.span_empty]

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