English
The lower central series is a descending chain: for every n, γ_{n+1}(G) ≤ γ_n(G).
Русский
Нижняя центральная последовательность образует нисходящую цепь: для каждого n выполняется γ_{n+1}(G) ≤ γ_n(G).
LaTeX
$$$\\forall n, \\lowerCentralSeries G (n+1) \\le \\lowerCentralSeries G n$$$
Lean4
theorem lowerCentralSeries_antitone : Antitone (lowerCentralSeries G) :=
by
refine antitone_nat_of_succ_le fun n x hx => ?_
simp only [mem_lowerCentralSeries_succ_iff, mem_top, true_and] at hx
refine closure_induction ?_ (Subgroup.one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx
rintro y ⟨z, hz, a, ha⟩
rw [← ha, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]
exact mul_mem hz (Normal.conj_mem (lowerCentralSeries_normal n) z⁻¹ (inv_mem hz) a)
