col_eq_prod — Mathlib

English

The j-th column is the Cartesian product of the index range up to μ.colLen(j) with the singleton {j}.

Русский

j-й столбец есть декартово произведение диапазона индексов до μ.colLen(j) и множества {j}.

LaTeX

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

Lean4

theorem col_eq_prod {μ : YoungDiagram} {j : ℕ} : μ.col j = Finset.range (μ.colLen j) ×ˢ { j } :=
  by
  ext ⟨a, b⟩
  simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_col_iff, mem_iff_lt_colLen, and_comm,
    and_congr_right_iff]
  rintro rfl
  rfl

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