succAbove_rev_right — Mathlib

English

For p ∈ Fin(n+1) and i ∈ Fin n, p.succAbove i.rev = (p.rev.succAbove i).rev.

Русский

Для p ∈ Fin(n+1) и i ∈ Fin n выполняется p.succAbove i.rev = (p.rev.succAbove i).rev.

LaTeX

$$$\forall p:\mathrm{Fin}(n+1),\forall i:\mathrm{Fin}(n),\ p.\mathrm{succAbove} (i.\mathrm{rev}) = (\mathrm{rev} \; p).\mathrm{succAbove} (i.\mathrm{rev}).$$$

Lean4

theorem succAbove_rev_right (p : Fin (n + 1)) (i : Fin n) : p.succAbove i.rev = (p.rev.succAbove i).rev := by
  rw [succAbove_rev_left, rev_rev]

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