mono_lie — Mathlib

English

If I ≤ J and N ≤ N', then [I,N] ≤ [J,N'].

Русский

Если I ≤ J и N ≤ N', то [I,N] ≤ [J,N'].

LaTeX

$$$$ \text{If } I \le J \text{ and } N \le N' , \; [I,N] \le [J,N'].$$$$

Lean4

@[gcongr]
theorem mono_lie (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆ :=
  by
  intro m h
  rw [lieIdeal_oper_eq_span, mem_lieSpan] at h; rw [lieIdeal_oper_eq_span, mem_lieSpan]
  intro N hN; apply h; rintro m' ⟨⟨x, hx⟩, ⟨n, hn⟩, hm⟩; rw [← hm]; apply hN
  use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩

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