predAbove_rev_right — Mathlib

English

Let n ∈ ℕ, p ∈ Fin(n), i ∈ Fin(n+1). Then p.predAbove(i.rev) = (p.rev.predAbove(i)).rev.

Русский

Пусть n ∈ ℕ, p ∈ Fin(n), i ∈ Fin(n+1). Тогда p.predAbove(i.rev) = (p.rev.predAbove(i)).rev.

LaTeX

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

Lean4

theorem predAbove_rev_right (p : Fin n) (i : Fin (n + 1)) : p.predAbove i.rev = (p.rev.predAbove i).rev := by
  rw [predAbove_rev_left, rev_rev]

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