last_eraseLast_le — Mathlib

English

The last element of eraseLast is below the last element of the original series.

Русский

Последний элемент eraseLast не превосходит последнего элемента исходной серии.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X),\\ (\\mathrm{RelSeries}.eraseLast\\ s).\\mathrm{last} \\le \\mathrm{RelSeries}.last\\ s.$$$

Lean4

theorem last_eraseLast_le (s : CompositionSeries X) : s.eraseLast.last ≤ s.last := by
  simp [eraseLast, last, s.strictMono.le_iff_le, Fin.le_iff_val_le_val]

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