ofRowLens — Mathlib

English

The j-th column equals Finset.range(μ.colLen(j)) × { j }. This describes all cells (i,j) with i ranging from 0 to μ.colLen(j)−1.

Русский

j-й столбец равен Finset.range(μ.colLen(j)) × { j }, то есть все клетки (i,j) с i от 0 до μ.colLen(j)−1.

LaTeX

$$$$ \mu.col(j) = \mathrm{Finset.range}(\mu.colLen(j)) \times \{ j \}. $$$$

Lean4

/-- Young diagram from a sorted list -/
def ofRowLens (w : List ℕ) (hw : w.Sorted (· ≥ ·)) : YoungDiagram
    where
  cells := YoungDiagram.cellsOfRowLens w
  isLowerSet := by
    rintro ⟨i2, j2⟩ ⟨i1, j1⟩ ⟨hi : i1 ≤ i2, hj : j1 ≤ j2⟩ hcell
    rw [Finset.mem_coe, YoungDiagram.mem_cellsOfRowLens] at hcell ⊢
    obtain ⟨h1, h2⟩ := hcell
    refine ⟨hi.trans_lt h1, ?_⟩
    calc
      j1 ≤ j2 := hj
      _ < w[i2] := h2
      _ ≤ w[i1] := by
        obtain rfl | h := eq_or_lt_of_le hi
        · rfl
        · exact List.pairwise_iff_get.mp hw _ _ h

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