span_sup

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.span_sup

English

The join of p with span s is the span of the union.

Русский

Соединение p с span s равно span от объединения.

LaTeX

$$$$ p \;⊔\; \operatorname{span} R s = \operatorname{span} R (s \cup \mathrm{setLike.coe}(p)) $$$$

Lean4

theorem span_sup : span R s ⊔ p = span R (s ∪ p) := by rw [Submodule.span_union, p.span_eq]

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

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

Разделы

Аффилиация

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