Documentation

Mathlib.Data.Fin.Rev

Reverse on Fin n #

This file contains lemmas about Fin.rev : Fin n → Fin n which maps i to n - 1 - i.

Definitions #

def Fin.revPerm {n : } :

Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by i ↦ n-(i+1).

Equations
@[simp]
theorem Fin.revPerm_apply {n : } (i : Fin n) :
@[simp]
theorem Fin.revPerm_symm_apply {n : } (i : Fin n) :
theorem Fin.cast_rev {n m : } (i : Fin n) (h : n = m) :
theorem Fin.rev_eq_iff {n : } {i j : Fin n} :
i.rev = j i = j.rev
theorem Fin.rev_ne_iff {n : } {i j : Fin n} :
i.rev j i j.rev
theorem Fin.rev_lt_iff {n : } {i j : Fin n} :
i.rev < j j.rev < i
theorem Fin.rev_le_iff {n : } {i j : Fin n} :
i.rev j j.rev i
theorem Fin.lt_rev_iff {n : } {i j : Fin n} :
i < j.rev j < i.rev
theorem Fin.le_rev_iff {n : } {i j : Fin n} :
i j.rev j i.rev
@[simp]
theorem Fin.val_rev_zero {n : } [NeZero n] :
(rev 0) = n.pred
theorem Fin.rev_pred {n : } {i : Fin (n + 1)} (h : i 0) (h' : i.rev last n := ) :
(i.pred h).rev = i.rev.castPred h'
theorem Fin.rev_castPred {n : } {i : Fin (n + 1)} (h : i last n) (h' : i.rev 0 := ) :
(i.castPred h).rev = i.rev.pred h'
theorem Fin.succAbove_rev_left {n : } (p : Fin (n + 1)) (i : Fin n) :
theorem Fin.succAbove_rev_right {n : } (p : Fin (n + 1)) (i : Fin n) :
theorem Fin.rev_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :

rev commutes with succAbove.

theorem Fin.predAbove_rev_left {n : } (p : Fin n) (i : Fin (n + 1)) :
theorem Fin.predAbove_rev_right {n : } (p : Fin n) (i : Fin (n + 1)) :
theorem Fin.rev_predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :

rev commutes with predAbove.

theorem Fin.add_rev_cast {n : } (j : Fin (n + 1)) :
j + j.rev = n
theorem Fin.rev_add_cast {n : } (j : Fin (n + 1)) :
j.rev + j = n