sup_span

Mathlib.LinearAlgebra.Span.Defs

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

English

As above, Nat-span equals AddSubmonoid closure.

Русский

Как выше, Span Nat равен замыканию AddSubmonoid.

LaTeX

$$$$ (\operatorname{span} \mathbb{N} s).\text{toAddSubmonoid} = \operatorname{AddSubmonoid}.closure s $$$$

Lean4

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

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

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

Разделы

Аффилиация

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