row_weak_of_le — Mathlib

English

If j1 ≤ j2 and (i,j2) ∈ μ, then T(i,j1) ≤ T(i,j2).

Русский

Если j1 ≤ j2 и (i,j2) ∈ μ, тогда T(i,j1) ≤ T(i,j2).

LaTeX

$$$\forall \mu\; T:\mathrm{SemistandardYoungTableau}(\mu),\; j1\le j2:\; (i,j2)\in \mu\Rightarrow T(i,j1) \le T(i,j2).$$$

Lean4

theorem row_weak_of_le {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j1 j2 : ℕ} (hj : j1 ≤ j2)
    (cell : (i, j2) ∈ μ) : T i j1 ≤ T i j2 :=
  by
  rcases eq_or_lt_of_le hj with h | h
  · rw [h]
  · exact T.row_weak h cell

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