English
For a Pi-type product ∀ i, Gs i, the nth term of the lower central series is bounded componentwise by the corresponding Pi of the factors.
Русский
Для произведения по индексу Пи ∀ i, Gs i, j-й элемент нижней центральной последовательности ограничен по компонентам соответствующими элементами факторов.
LaTeX
$$$\\operatorname{lowerCentralSeries}(\\prod_i Gs_i, n) \\le \\operatorname{pi}(\\{i\\}, \\operatorname{lowerCentralSeries}(Gs_i, n))$$$
Lean4
theorem lowerCentralSeries_pi_le (n : ℕ) :
lowerCentralSeries (∀ i, Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n :=
by
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f
induction n with
| zero => simp [pi_top]
| succ n ih =>
calc
lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
_ ≤ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_mono ih (le_refl _))
_ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi, pi_top]
_ ≤ pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_pi_pi_le _ _)
_ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
