English
In a composition series, each successive step is strictly below the next: s(i.castSucc) < s(i.succ).
Русский
В составной серии каждый следующий элемент строго превышает предыдущий: s(i.castSucc) < s(i.succ).
LaTeX
$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ (s : \\mathrm{CompositionSeries}\\ X)\\, (i : \\mathrm{Fin}\\ s.length),\\ s(\\mathrm{Fin.castSucc}\\ i) < s(\\mathrm{Fin.succ}\\ i).$$$
Lean4
/-- A `CompositionSeries X` is a finite nonempty series of elements of a
`JordanHolderLattice` such that each element is maximal inside the next. The length of a
`CompositionSeries X` is one less than the number of elements in the series.
Note that there is no stipulation that a series start from the bottom of the lattice and finish at
the top. For a composition series `s`, `s.last` is the largest element of the series,
and `s.head` is the least element.
-/
abbrev CompositionSeries (X : Type u) [Lattice X] [JordanHolderLattice X] : Type u :=
RelSeries {(x, y) : X × X | IsMaximal x y}
