span_sup

Mathlib.LinearAlgebra.Projectivization.Subspace

URI: https://scilib.ai/kg/mathlib#Projectivization.Subspace.span_sup

English

The supremum of a set and a span is the span of their union.

Русский

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

LaTeX

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

Lean4

theorem span_sup {S : Set (ℙ K V)} {W : Subspace K V} : span S ⊔ W = span (S ∪ W) := by rw [span_union, span_coe]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru