getD_reverse — Mathlib

English

For any list l and index i within bounds, getD of the reversed list at i equals getD of the original list at length(l) - 1 - i.

Русский

Для списка l и индекса i, лежащего в пределах, getD для обращенного списка на i равно getD исходного списка на длину(l) - 1 - i.

LaTeX

$$$$ \\forall l,\\forall i<|l|,\\ \\mathrm{getD}(l^{\\text{rev}}, i) = \\mathrm{getD}(l, |l|-1-i). $$$$

Lean4

theorem getD_reverse {l : List α} (i) (h : i < length l) : getD l.reverse i = getD l (l.length - 1 - i) :=
  by
  funext a
  rwa [List.getD_eq_getElem?_getD, List.getElem?_reverse, ← List.getD_eq_getElem?_getD]

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