Theorems · Definition · combinatorics

SemistandardYoungTableau.mk.noConfusion

{μ : YoungDiagram} →
  {P : Sort u} →
    {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' : ℕ → ℕ → ℕ} →
              {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 := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' } =
                        { entry := entry', row_weak' := row_weak'', col_strict' := col_strict'', zeros' := zeros'' } →
                      (entry = entry' → P) → P

Defined in

Mathlib.Combinatorics.Young.SemistandardTableau

Cited by

1 results in Mathlib

Foundations

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