Theorems · Theorem · combinatorics

SemistandardYoungTableau.mk.inj

∀ {μ : YoungDiagram} {entry : ℕ → ℕ → ℕ} {row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2}
  {col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j}
  {zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0} {entry_1 : ℕ → ℕ → ℕ}
  {row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2}
  {col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j}
  {zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0},
  { entry := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' } =
      { entry := entry_1, row_weak' := row_weak'_1, col_strict' := col_strict'_1, zeros' := zeros'_1 } →
    entry = entry_1

Defined in

Mathlib.Combinatorics.Young.SemistandardTableau

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound