English
A sequence H(n) of subgroups is ascending central if H(0)=⊥ and for all x ∈ G and n, x ∈ H(n+1) implies ∀ g ∈ G, x g x^{-1} g^{-1} ∈ H(n).
Русский
Последовательность подгрупп H(n) восходящая центральная, если H(0)=⊥ и для любых x∈G, n, если x∈H(n+1), то для всех g∈G выполняется x g x^{-1} g^{-1} ∈ H(n).
LaTeX
$$$\text{IsAscendingCentralSeries}(H) := H(0)=\perp \wedge \forall x\in G,\forall n,\ x\in H(n+1)\Rightarrow \forall g\in G,\ xgx^{-1}g^{-1}\in H(n).$$$
Lean4
/-- A sequence of subgroups of `G` is an ascending central series if `H 0` is trivial and
`⁅H (n + 1), G⁆ ⊆ H n` for all `n`. Note that we do not require that `H n = G` for some `n`. -/
def IsAscendingCentralSeries (H : ℕ → Subgroup G) : Prop :=
H 0 = ⊥ ∧ ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ g, x * g * x⁻¹ * g⁻¹ ∈ H n
