span_iUnion

Mathlib.LinearAlgebra.Span.Defs

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

English

Span of a union over an index equals the supremum of spans over the index.

Русский

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

LaTeX

$$$$\operatorname{span} R\Big( \bigcup_i s_i \Big) = \bigvee_i \operatorname{span} R (s_i)$$$$

Lean4

theorem span_iUnion {ι} (s : ι → Set M) : span R (⋃ i, s i) = ⨆ i, span R (s i) :=
  (Submodule.gi R M).gc.l_iSup

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

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

Разделы

Аффилиация

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