stk_nth_val — Mathlib

English

For a list L whose k-projection matches a reversed list S, the kth nth value L.nth n k equals the corresponding element of S reversed.

Русский

Для списка L, проекция которого на k совпадает с обращённым списком S, значение L.nth n k равно соответствующему элементу S.reverse n.

LaTeX

$$$ L.nth\;n\;k = S.reverse\;[n] ? $$$

Lean4

theorem stk_nth_val {K : Type*} {Γ : K → Type*} {L : ListBlank (∀ k, Option (Γ k))} {k S} (n)
    (hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse) : L.nth n k = S.reverse[n]? :=
  by
  rw [← proj_map_nth, hL, ← List.map_reverse, ListBlank.nth_mk, List.getI_eq_iget_getElem?, List.getElem?_map]
  cases S.reverse[n]? <;> rfl

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