rowLens_ofRowLens_eq_self — Mathlib

English

For any w with hw, the diagram obtained from w has rowLens equal to w.

Русский

Для любого w, удовлетворяющего hw, диаграмма, полученная по w, имеет rowLens, равный w.

LaTeX

$$$$\operatorname{rowLens}\left(\operatorname{ofRowLens}(w,hw)\right) = w.$$$$

Lean4

/-- The right_inv direction of the equivalence -/
theorem rowLens_ofRowLens_eq_self {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (hpos : ∀ x ∈ w, 0 < x) :
    (ofRowLens w hw).rowLens = w :=
  List.ext_get (rowLens_length_ofRowLens hpos) fun i h₁ h₂ => (get_rowLens (h := h₁)).trans <| rowLen_ofRowLens ⟨i, h₂⟩

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