next_reverse_eq_prev — Mathlib

English

The next element in the reversed list is the predecessor in the original: next(l.reverse) x = prev(l) x.

Русский

Следующий элемент в перевернутом списке равен предшественнику в исходном списке: next(l.reverse) x = prev(l) x.

LaTeX

$$$next\ l.reverse\ x\ (mem\_reverse.mpr\ hx) = \text{prev}(l)\ x\ hx$$$

Lean4

theorem next_reverse_eq_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) :
    next l.reverse x (mem_reverse.mpr hx) = prev l x hx :=
  by
  convert (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm
  exact (reverse_reverse l).symm

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