lt_succ — Mathlib

English

The toList of a composition series is sorted with respect to the relation <.

Русский

Список элементов композиционной серии упорядочен по отношению <.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X),\\ (RelSeries.toList s)\\ \\mathrm{Sorted}\\ (<).$$$

Lean4

theorem lt_succ (s : CompositionSeries X) (i : Fin s.length) : s (Fin.castSucc i) < s (Fin.succ i) :=
  lt_of_isMaximal (s.step _)

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