rev_succAbove — Mathlib

English

rev commutes with succAbove: rev(succAbove p i) = succAbove(rev p)(rev i).

Русский

rev коммутирует с succAbove: rev(succAbove p i) = succAbove(rev p)(rev i).

LaTeX

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

Lean4

/-- `rev` commutes with `succAbove`. -/
theorem rev_succAbove (p : Fin (n + 1)) (i : Fin n) : rev (succAbove p i) = succAbove (rev p) (rev i) := by
  rw [succAbove_rev_left, rev_rev]

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