Theorems · Theorem · combinatorics

SemistandardYoungTableau.mk.injEq

∀ {μ : 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

0 results in Mathlib

Foundations

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