row_weak — Mathlib

English

In a semistandard tableau, entries weakly increase along a row.

Русский

В семистандартной таблице значения неубывают по строке слева направо.

LaTeX

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

Lean4

theorem row_weak {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j1 j2 : ℕ} (hj : j1 < j2)
    (hcell : (i, j2) ∈ μ) : T i j1 ≤ T i j2 :=
  T.row_weak' hj hcell

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