get_reverse' — Mathlib

English

For any list l and any index n, the nth element of l reversed is the element of l at position length(l) - 1 - n, when n is a valid index into the reversed list.

Русский

Для любого списка l и индекса n, n-й элемент списка l в обратном порядке равен элементу l на позиции length(l) - 1 - n, если этот индекс допустим.

LaTeX

$$$\\\\forall l:\\\\, \\text{List }\\\\alpha, \\\\forall n \\\\in \\mathbb{N}, \\\\ n < |l^{\\\\mathrm{rev}}| \\\\Rightarrow (l^{\\\\mathrm{rev}})_n = l_{|l| - 1 - n}.$$$

Lean4

theorem get_reverse' (l : List α) (n) (hn') : l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩ := by simp

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