rev_predAbove — Mathlib

English

The reverse operation commutes with predAbove: (predAbove p i).rev = predAbove p.rev i.rev.

Русский

Обратное отображение коммутирует с predAbove: (predAbove p i).rev = predAbove p.rev i.rev.

LaTeX

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

Lean4

/-- `rev` commutes with `predAbove`. -/
theorem rev_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : (predAbove p i).rev = predAbove p.rev i.rev := by
  rw [predAbove_rev_left, rev_rev]

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