antitone_lowerCentralSeries — Mathlib

English

If the module is Artinian, then there exists n such that for all l at least n, the infimum over k of lcs_k equals lcs_l.

Русский

Если модуль является артиновым, существует n, что для всех l ≥ n выполняется, что iInf_k lcs_k = lcs_l.

LaTeX

$$$\\exists n, \\forall l \\ge n, \\; \\bigwedge_{k} lcs_k = lcs_l$$$

Lean4

theorem antitone_lowerCentralSeries : Antitone <| lowerCentralSeries R L M :=
  by
  intro l k
  induction k generalizing l with
  | zero => exact fun h ↦ (Nat.le_zero.mp h).symm ▸ le_rfl
  | succ k ih =>
    intro h
    rcases Nat.of_le_succ h with (hk | hk)
    · rw [lowerCentralSeries_succ]
      exact (LieSubmodule.mono_lie_right ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
    · exact hk.symm ▸ le_rfl

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