span_union

Mathlib.RingTheory.Ideal.Span

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

English

The span of a union equals the join of spans: span(s ∪ t) = span(s) ⊔ span(t).

Русский

Покрытие объединения равно объединению порождений: span(s ∪ t) = span(s) ⊔ span(t).

LaTeX

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

Lean4

theorem span_union (s t : Set α) : span (s ∪ t) = span s ⊔ span t :=
  Submodule.span_union _ _

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

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

Разделы

Аффилиация

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