mem_cellsOfRowLens — Mathlib

English

For any w and c = (i,j), c ∈ cellsOfRowLens(w) iff i < |w| and j < w[i].

Русский

Для списка w и клетки c=(i,j) верно: c ∈ cellsOfRowLens(w) тогда и только если i < |w| и j < w[i].

LaTeX

$$$$ c \in \mathrm{cellsOfRowLens}(w) \iff (i < |w|) \wedge (j < w[i]) \quad \text{где } c=(i,j). $$$$

Lean4

protected theorem mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} :
    c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h : c.fst < w.length, c.snd < w[c.fst] :=
  by
  induction w generalizing c <;> rw [YoungDiagram.cellsOfRowLens]
  · simp
  · rcases c with ⟨⟨_, _⟩, _⟩ <;> simp_all

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