col_strict

Mathlib.Combinatorics.Young.SemistandardTableau

URI: https://scilib.ai/kg/mathlib#SemistandardYoungTableau.col_strict

← MathLib Explorer

English

Columns are strictly increasing: if i1 < i2 and (i2,j) is in μ, then T(i1,j) < T(i2,j).

Русский

Столбцы строго возрастают: если i1 < i2 и (i2,j) в μ, то T(i1,j) < T(i2,j).

LaTeX

$$$\forall \mu\; T:\mathrm{SemistandardYoungTableau}(\mu),\; i_1

Lean4

theorem col_strict {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 i2 j : ℕ} (hi : i1 < i2)
    (hcell : (i2, j) ∈ μ) : T i1 j < T i2 j :=
  T.col_strict' hi hcell

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

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

Разделы

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

Аффилиация

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