derivedSeriesOfIdeal_le — Mathlib

English

For k,l, the k-th derived series of I plus J dominates the sum of the k-th and l-th terms: D(k+l)(I+J) ≤ D(k)I + D(l)J.

Русский

Для k,l производный ряд I+J не хуже суммы D(k)I и D(l)J: D(k+l)(I+J) ≤ D(k)I + D(l)J.

LaTeX

$$$D(k+l)(I+J) \leq D(k)I + D(l)J$$$

Lean4

@[gcongr, mono]
theorem derivedSeriesOfIdeal_le {I J : LieIdeal R L} {k l : ℕ} (h₁ : I ≤ J) (h₂ : l ≤ k) : D k I ≤ D l J := by
  induction k generalizing l with
  | zero => rw [le_zero_iff] at h₂; rw [h₂, derivedSeriesOfIdeal_zero]; exact h₁
  | succ k ih =>
    have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
    rcases h with h | h
    · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
      exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
    · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

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