le_last — Mathlib

English

For any s, i with i in Fin(s.length+1), s i ≤ s.last.

Русский

Для любого индекса в композиционной серии элементы не превосходят последний элемент серии.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ \\forall {s : \\mathrm{CompositionSeries}\\ X} \\ \\forall {i : \\mathrm{Fin}(s.length + 1)},\\ s i \\le s.{\\text{last}}.$$$

Lean4

@[simp]
theorem le_last {s : CompositionSeries X} (i : Fin (s.length + 1)) : s i ≤ s.last :=
  s.strictMono.monotone (Fin.le_last _)

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