ascending_central_series_le_upper

English

The upper central series is an ascending central series.

Русский

Верхняя центральная серия является восходящей центральной серией.

LaTeX

$$$\text{IsAscendingCentralSeries}(\mathrm{upperCentralSeries}(G))$$$

Lean4

/-- Any ascending central series for a group is bounded above by the upper central series. -/
theorem ascending_central_series_le_upper (H : ℕ → Subgroup G) (hH : IsAscendingCentralSeries H) :
    ∀ n : ℕ, H n ≤ upperCentralSeries G n
  | 0 => hH.1.symm ▸ le_refl ⊥
  | n + 1 => by
    intro x hx
    rw [mem_upperCentralSeries_succ_iff]
    exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

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