derivedSeries_eq_top — Mathlib

English

If for some n the (n+1)-st derived series is top, then all higher derived series are top, and conversely the base case implies the rest.

Русский

Если для некоторого n-ая (n+1)-я производящая серия равна верхнему пределу, тогда все более высокие производящие серии также равны верхнему пределу; и наоборот, базовый случай задаёт остальные.

LaTeX

$$$\mathrm{derivedSeries}_{R} L (n+1) = \top \rightarrow \mathrm{derivedSeries}_{R} L n = \top$$$

Lean4

theorem derivedSeries_eq_top (n : ℕ) (h : derivedSeries R L 1 = ⊤) : derivedSeries R L n = ⊤ :=
  by
  cases n
  · rfl
  · rwa [derivedSeries_succ_eq_top_iff]

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