span_iUnion

Mathlib.Algebra.Lie.Submodule

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

English

Lie-span commutes with arbitrary unions: lieSpan R L (⋃ i, s i) = ⨆ i, lieSpan R L (s i).

Русский

Lie-span сохраняет произвольные объединения: lieSpan(⋃ i s_i) = ⨆ i lieSpan(s_i).

LaTeX

$$lieSpan_{R,L}(\\bigcup_i s_i) = \\bigvee_i lieSpan_{R,L}(s_i)$$

Lean4

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

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

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

Разделы

Аффилиация

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