rowLen_ofRowLens — Mathlib

English

For any w with hw, the i-th row length of the diagram built from w equals w[i].

Русский

Для любого списка w с доказательством упорядоченности hw i-я длина ряда диаграммы, образованной по w, равна w[i].

LaTeX

$$$$\bigl(\operatorname{ofRowLens}(w,hw)\bigr).\operatorname{rowLen}(i) = w[i].$$$$

Lean4

/-- The length of the `i`th row in `ofRowLens w hw` is the `i`th entry of `w` -/
theorem rowLen_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (i : Fin w.length) : (ofRowLens w hw).rowLen i = w[i] :=
  by simp [rowLen, Nat.find_eq_iff, mem_ofRowLens]

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