up_left_mem — Mathlib

English

Let μ be a Young diagram. If i1 ≤ i2 and j1 ≤ j2 and (i2, j2) ∈ μ, then (i1, j1) ∈ μ.

Русский

Пусть μ — диаграмма Юнга. Если i1 ≤ i2 и j1 ≤ j2 и (i2, j2) ∈ μ, тогда (i1, j1) ∈ μ.

LaTeX

$$$ \forall \mu \; \forall i_1,i_2,j_1,j_2 \in \mathbb{N},\; i_1 \le i_2 \land j_1 \le j_2 \land (i_2,j_2) \in \mu \Rightarrow (i_1,j_1) \in \mu.$$$

Lean4

/-- In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2)
means (i1, j1) is weakly up-and-left of (i2, j2). -/
theorem up_left_mem (μ : YoungDiagram) {i1 i2 j1 j2 : ℕ} (hi : i1 ≤ i2) (hj : j1 ≤ j2) (hcell : (i2, j2) ∈ μ) :
    (i1, j1) ∈ μ :=
  μ.isLowerSet (Prod.mk_le_mk.mpr ⟨hi, hj⟩) hcell

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