span_union — Mathlib

English

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

Русский

Порождающее объединение равно объединению порождений: lieSpan_R L(s ∪ t) = lieSpan_R L s ⊔ lieSpan_R L t.

LaTeX

$$$\\operatorname{lieSpan}_R L(s\\cup t) = \\operatorname{lieSpan}_R L(s) \\vee \\operatorname{lieSpan}_R L(t)$$$

Lean4

theorem span_union (s t : Set L) : lieSpan R L (s ∪ t) = lieSpan R L s ⊔ lieSpan R L t :=
  (LieSubalgebra.gi R L).gc.l_sup

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