col_weak — Mathlib

English

If i1 ≤ i2 and (i2,j) ∈ μ, then T(i1,j) ≤ T(i2,j).

Русский

Если i1 ≤ i2 и (i2,j) в μ, тогда T(i1,j) ≤ T(i2,j).

LaTeX

$$$\forall \mu\; T:\mathrm{SemistandardYoungTableau}(\mu),\; i1\le i2:\; (i2,j)\in \mu\Rightarrow T(i1,j) \le T(i2,j).$$$

Lean4

theorem col_weak {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i1 i2 j : ℕ} (hi : i1 ≤ i2) (cell : (i2, j) ∈ μ) :
    T i1 j ≤ T i2 j := by
  rcases eq_or_lt_of_le hi with h | h
  · rw [h]
  · exact le_of_lt (T.col_strict h cell)

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