lcs_sup — Mathlib

English

The generalized lower central series commutes with joins: (N1 ⊔ N2).lcs k = N1.lcs k ⊔ N2.lcs k.

Русский

Операция lcs сопряжена с объединением: (N1 ⊔ N2).lcs k = N1.lcs k ⊔ N2.lcs k.

LaTeX

$$ (N1 ⊔ N2).lcs k = N1.lcs k ⊔ N2.lcs k $$

Lean4

@[simp]
theorem lcs_sup {N₁ N₂ : LieSubmodule R L M} {k : ℕ} : (N₁ ⊔ N₂).lcs k = N₁.lcs k ⊔ N₂.lcs k := by
  induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

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