span_iUnion — Mathlib

English

The span over an indexed union equals the supremum of the spans: lieSpan_R L(⋃ i, s_i) = ⨆ i, lieSpan_R L(s_i).

Русский

Порождение по объединению по индексу равно верхней границе порождений: lieSpan_R L(⋃_i s_i) = ⨆_i lieSpan_R L(s_i).

LaTeX

$$$\\operatorname{lieSpan}_R L\\big(\\bigcup_i s_i\\big) = \\bigvee_i \\operatorname{lieSpan}_R L(s_i)$$$

Lean4

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

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