row — Mathlib

English

The i-th row of a Young diagram consists of the cells whose first coordinate is i.

Русский

Не́сение i-й строки диаграммы Юнга состоит из клеток, чьи первая координата равна i.

LaTeX

$$$ \text{row}(μ,i) = \{(a,b) \in μ.cells \mid a = i\}. $$$

Lean4

/-- The `i`-th row of a Young diagram consists of the cells whose first coordinate is `i`. -/
def row (μ : YoungDiagram) (i : ℕ) : Finset (ℕ × ℕ) :=
  μ.cells.filter fun c => c.fst = i

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