English
Bracket distributes over sup: [I ⊔ J, N] = [I,N] ⊔ [J,N].
Русский
Скобка распределяется по объединению: [I ⊔ J, N] = [I,N] ⊔ [J,N].
LaTeX
$$$$ [I \sqcup J, N] = [I,N] \sqcup [J,N]. $$$$
Lean4
@[simp]
theorem lie_sup : ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆ :=
by
have h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆ := by rw [sup_le_iff];
constructor <;> apply mono_lie_right <;> [exact le_sup_left; exact le_sup_right]
suffices ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆ by exact le_antisymm this h
rw [lieIdeal_oper_eq_span, lieSpan_le]
rintro m ⟨x, ⟨n, hn⟩, h⟩
simp only [SetLike.mem_coe]
rw [LieSubmodule.mem_sup] at hn ⊢
rcases hn with ⟨n₁, hn₁, n₂, hn₂, hn'⟩
use ⁅(x : L), (⟨n₁, hn₁⟩ : N)⁆; constructor; · apply lie_coe_mem_lie
use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆; constructor; · apply lie_coe_mem_lie
simp [← h, ← hn']
