rowLens_sorted — Mathlib

English

The sequence rowLens is nonincreasing: RowLens is sorted with respect to ≥.

Русский

Последовательность rowLens не возрастает: RowLens упорядочена по неубыванию в направлении ≥.

LaTeX

$$$$ \mathrm{RowLens} \text{ is sorted: } \mathrm{RowLens} \ge \!\! \text{ (pointwise)}. $$$$

Lean4

theorem rowLens_sorted (μ : YoungDiagram) : μ.rowLens.Sorted (· ≥ ·) :=
  List.pairwise_le_range.map _ μ.rowLen_anti

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