ofRowLens_to_rowLens_eq_self — Mathlib

English

For any Young diagram μ, reconstructing μ from its row-length list yields μ itself. In other words, the diagram is the left-inverse of the forward map.

Русский

Для любой диаграммы Янга повторное построение диаграммы по списку длин её рядов и отсортированному списку возвращает исходную диаграмму.

LaTeX

$$$$\operatorname{ofRowLens}\left(\operatorname{rowLens}(\mu), \operatorname{rowLens_sorted}(\mu)\right) = \mu.$$$$

Lean4

/-- The left_inv direction of the equivalence -/
theorem ofRowLens_to_rowLens_eq_self {μ : YoungDiagram} : ofRowLens _ (rowLens_sorted μ) = μ :=
  by
  ext ⟨i, j⟩
  simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]
  simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt

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