descending_central_series_ge_lower

English

Given any descending central series H, γ_n(G) ≤ H_n for all n.

Русский

Для любой нисходящей центральной серии H выполнено γ_n(G) ≤ H_n для всех n.

LaTeX

$$$\\forall n, \\lowerCentralSeries G n \\le H n$ (при условии, что $H$ является нисходящей центральной серией).$$

Lean4

/-- Any descending central series for a group is bounded below by the lower central series. -/
theorem descending_central_series_ge_lower (H : ℕ → Subgroup G) (hH : IsDescendingCentralSeries H) :
    ∀ n : ℕ, lowerCentralSeries G n ≤ H n
  | 0 => hH.1.symm ▸ le_refl ⊤
  | n + 1 => commutator_le.mpr fun x hx q _ => hH.2 x n (descending_central_series_ge_lower H hH n hx) q

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