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