col — Mathlib

English

The j-th column of a diagram μ consists of all cells whose second coordinate equals j.

Русский

j-й столбец диаграммы μ состоит из клеток, чьи вторые координаты равны j.

LaTeX

$$$$ \mu.col(j) = \{ (i,k) \in \mathbb{N} \times \mathbb{N} \mid (i,k) \in \mu.cells \text{ and } k = j \}. $$$$

Lean4

/-- The `j`-th column of a Young diagram consists of the cells whose second coordinate is `j`. -/
def col (μ : YoungDiagram) (j : ℕ) : Finset (ℕ × ℕ) :=
  μ.cells.filter fun c => c.snd = j

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