row_eq_prod — Mathlib

English

The i-th row is exactly the Cartesian product of the index i with the initial segment of length μ.rowLen(i): the set of pairs (i,k) with k = 0,1,...,μ.rowLen(i)−1.

Русский

i-я строка равна произведению {i} × Finset.range(μ.rowLen(i)); то есть пары (i,k) с k = 0,1,...,μ.rowLen(i)−1.

LaTeX

$$$$ \mu.row(i) = \{ i \} \times\! \mathrm{Finset.range}(\mu.rowLen(i)). $$$$

Lean4

theorem row_eq_prod {μ : YoungDiagram} {i : ℕ} : μ.row i = { i } ×ˢ Finset.range (μ.rowLen i) :=
  by
  ext ⟨a, b⟩
  simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff, mem_iff_lt_rowLen, and_comm,
    and_congr_right_iff]
  rintro rfl
  rfl

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