cellsOfRowLens — Mathlib

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 ℕ))

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