span_union — Mathlib

English

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

Русский

lie-span объединения равен объединениюLie-span каждого множества: lieSpan(s ∪ t) = lieSpan(s) ⊔ lieSpan(t).

LaTeX

$$lieSpan_{R,L}(s \\cup t) = \\operatorname{lieSpan}_{R,L}(s) \\; \\sqcup \\; \\operatorname{lieSpan}_{R,L}(t)$$

Lean4

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

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