mem_ofRowLens

Mathlib.Combinatorics.Young.YoungDiagram

URI: https://scilib.ai/kg/mathlib#YoungDiagram.mem_ofRowLens

← MathLib Explorer

English

colLen j equals the cardinality of the j-th column: colLen j = (col j).card.

Русский

colLen(j) равна кардиналу j-го столбца: colLen(j) = (col j).card.

LaTeX

$$$$ \mu.colLen(j) = (\mu.col(j)).card. $$$$

Lean4

theorem mem_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} {c : ℕ × ℕ} :
    c ∈ ofRowLens w hw ↔ ∃ h : c.fst < w.length, c.snd < w[c.fst] :=
  YoungDiagram.mem_cellsOfRowLens

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru