toList_sorted — Mathlib

English

The toList of a CompositionSeries is sorted with respect to <.

Русский

Список toList композиционной серии отсортирован относительно порядка <.

LaTeX

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

Lean4

theorem toList_sorted (s : CompositionSeries X) : s.toList.Sorted (· < ·) :=
  List.pairwise_iff_get.2 fun i j h => by
    dsimp only [RelSeries.toList]
    rw [List.get_ofFn, List.get_ofFn]
    exact s.strictMono h

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