sup_span — Mathlib

English

The supremum of a subspace W and the span of a set S equals the span of the union W ∪ S.

Русский

Супремум подпространства W и span множества S равен span объединения W и S.

LaTeX

$$$W \vee \operatorname{span}(S) = \operatorname{span}(W \cup S)$$$

Lean4

/-- The supremum of a subspace and the span of a set of points is equal to the span of the union of
the subspace and the set of points. -/
theorem sup_span {S : Set (ℙ K V)} {W : Subspace K V} : W ⊔ span S = span (W ∪ S) := by rw [span_union, span_coe]

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