English
Let w be a finite nonincreasing sequence of positive integers. The number of rows of the Young diagram formed from w equals the length of w.
Русский
Пусть w — конечная невозрастающая последовательность положительных целых чисел. Число строк диаграммы Янга, образованной по w, равно длине последовательности w.
LaTeX
$$$$\operatorname{length}\left(\operatorname{rowLens}\left(\operatorname{ofRowLens}(w,hw)\right)\right) = \operatorname{length}(w).$$$$
Lean4
/-- The number of rows in `ofRowLens w hw` is the length of `w` -/
theorem rowLens_length_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpos : ∀ x ∈ w, 0 < x) :
(ofRowLens w hw).rowLens.length = w.length :=
by
simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens, lt_self_iff_false, IsEmpty.exists_iff,
Classical.not_not]
exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩
