English
There is a bijection between Young diagrams and finite nonincreasing lists of positive integers, given by mapping to row lengths and back.
Русский
Существует биекция между диаграммами Янга и конечными невозрастающими списками положительных целых чисел, задаваемая переходами к длинам рядов и обратно.
LaTeX
$$$$\mathrm{YoungDiagram} \cong \{ w : \mathrm{List}(\mathbb{N}) \mid w_1 \ge w_2 \ge \cdots \ge w_k > 0\}.$$$
Lean4
/-- Equivalence between Young diagrams and weakly decreasing lists of positive natural numbers.
A Young diagram `μ` is equivalent to a list of row lengths. -/
@[simps]
def equivListRowLens : YoungDiagram ≃ { w : List ℕ // w.Sorted (· ≥ ·) ∧ ∀ x ∈ w, 0 < x }
where
toFun μ := ⟨μ.rowLens, μ.rowLens_sorted, μ.pos_of_mem_rowLens⟩
invFun ww := ofRowLens ww.1 ww.2.1
left_inv _ := ofRowLens_to_rowLens_eq_self
right_inv := fun ⟨_, hw⟩ => Subtype.mk_eq_mk.mpr (rowLens_ofRowLens_eq_self hw.2)
