derivedSeries_antitone

Mathlib.GroupTheory.Solvable

URI: https://scilib.ai/kg/mathlib#derivedSeries_antitone

English

The derived series is antitone: D_{n+1} ≤ D_n for all n.

Русский

Производящая серия антиупорядочена: D_{n+1} ≤ D_n для всех n.

LaTeX

$$For all n, $\\mathrm{derivedSeries}(G,n+1) \\le \\mathrm{derivedSeries}(G,n)$.$$

Lean4

theorem derivedSeries_antitone : Antitone (derivedSeries G) :=
  antitone_nat_of_succ_le fun n => (derivedSeries G n).commutator_le_self

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru