English
For any w and hw, and any c = (i,j), c ∈ ofRowLens(w,hw) iff ∃ h with h < |w| and j < w[i].
Русский
Для списка длин строк w и доказательства hw, для любой пары c = (i,j) верно: c ∈ ofRowLens(w,hw) тогда и только если ∃ h < |w|, j < w[i].
LaTeX
$$$$ c \in \mathrm{ofRowLens}(w,hw) \iff \exists h < |w| \text{ such that } j < w[i], \text{ где } c=(i,j). $$$$
Lean4
/-- The cells making up a `YoungDiagram` from a list of row lengths -/
protected def cellsOfRowLens : List ℕ → Finset (ℕ × ℕ)
| [] => ∅
| w :: ws =>
({0} : Finset ℕ) ×ˢ Finset.range w ∪
(YoungDiagram.cellsOfRowLens ws).map (Embedding.prodMap ⟨_, Nat.succ_injective⟩ (Embedding.refl ℕ))