span_union

Mathlib.LinearAlgebra.Span.Defs

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

English

The span of a union equals the supremum of the spans.

Русский

Порождающее объединение равно наибольшему элементу порождений.

LaTeX

$$$$\\operatorname{span} R (s \\cup t) = \\operatorname{span} R s \\;\\sqcup\\; \\operatorname{span} R t$$$$

Lean4

theorem span_union (s t : Set M) : span R (s ∪ t) = span R s ⊔ span R t :=
  (Submodule.gi R M).gc.l_sup

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

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

Разделы

Аффилиация

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