English
An auxiliary recursive construction produces a sequence of subgroups H_n of a group G, starting with H_0 = {e} and defining H_{n+1} from H_n via the centered-step operation; each H_n is normal in G.
Русский
Вспомогательная последовательность подгрупп H_n группы G задаётся рекурсивно: H_0 = {e} и H_{n+1} строится через центральный шаг по отношению к H_n; все H_n нормальны в G.
LaTeX
$$$\exists (H_n)_{n\in\mathbb{N}}:\mathbb{N}\to\mathrm{Subgroup}(G),\ H_0=\perp,\ \forall n,\ H_{n+1}=\{g\in G\;|\; gH_n\in Z(G/H_n)\},\ \forall n,\ H_n\trianglelefteq G.$$$
Lean4
/-- An auxiliary type-theoretic definition defining both the upper central series of
a group, and a proof that it is normal, all in one go. -/
def upperCentralSeriesAux : ℕ → Σ' H : Subgroup G, Normal H
| 0 => ⟨⊥, inferInstance⟩
| n + 1 =>
let un := upperCentralSeriesAux n
let _un_normal := un.2
⟨upperCentralSeriesStep un.1, inferInstance⟩
