isMaximal_eraseLast_last — Mathlib

English

For any Composition Series s with positive length, the last-1 element s.eraseLast.last is maximal below s.last.

Русский

Для любой композиционной последовательности s с положительной длиной последний-1 элемент s.eraseLast.last максимален ниже s.last.

LaTeX

$$$0< s.length \\Rightarrow IsMaximal(s.eraseLast.last, s.last).$$$

Lean4

theorem isMaximal_eraseLast_last {s : CompositionSeries X} (h : 0 < s.length) : IsMaximal s.eraseLast.last s.last :=
  by
  rw [last_eraseLast, last]
  have := s.step ⟨s.length - 1, by cutsat⟩
  simp only [Fin.castSucc_mk, Fin.succ_mk, mem_setOf_eq] at this
  convert this using 3
  exact (tsub_add_cancel_of_le h).symm

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