# Reverse on `Fin n` #

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

## Definitions #

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

source
theorem Fin.rev_involutive {n : ℕ} :
Function.Involutive rev
source
def Fin.revPerm {n : ℕ} :
Equiv.Perm (Fin n)

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

Equations

- Fin.revPerm = Function.Involutive.toPerm Fin.rev ⋯

Instances For

source
@[simp]
theorem Fin.revPerm_apply {n : ℕ} (i : Fin n) :
revPerm i = i.rev
source
@[simp]
theorem Fin.revPerm_symm_apply {n : ℕ} (i : Fin n) :
(Equiv.symm revPerm) i = i.rev
source
theorem Fin.rev_injective {n : ℕ} :
Function.Injective rev
source
theorem Fin.rev_surjective {n : ℕ} :
Function.Surjective rev
source
theorem Fin.rev_bijective {n : ℕ} :
Function.Bijective rev
source
@[simp]
theorem Fin.revPerm_symm {n : ℕ} :
Equiv.symm revPerm = revPerm
source
theorem Fin.cast_rev {n m : ℕ} (i : Fin n) (h : n = m) :
Fin.cast h i.rev = (Fin.cast h i).rev
source
theorem Fin.rev_eq_iff {n : ℕ} {i j : Fin n} :
i.rev = j ↔ i = j.rev
source
theorem Fin.rev_ne_iff {n : ℕ} {i j : Fin n} :
i.rev ≠ j ↔ i ≠ j.rev
source
theorem Fin.rev_lt_iff {n : ℕ} {i j : Fin n} :
i.rev < j ↔ j.rev < i
source
theorem Fin.rev_le_iff {n : ℕ} {i j : Fin n} :
i.rev ≤ j ↔ j.rev ≤ i
source
theorem Fin.lt_rev_iff {n : ℕ} {i j : Fin n} :
i < j.rev ↔ j < i.rev
source
theorem Fin.le_rev_iff {n : ℕ} {i j : Fin n} :
i ≤ j.rev ↔ j ≤ i.rev
source
theorem Fin.val_rev_zero {n : ℕ} [NeZero n] :
↑(rev 0) = n.pred
source
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'
source
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'
source
theorem Fin.succAbove_rev_left {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
p.rev.succAbove i = (p.succAbove i.rev).rev
source
theorem Fin.succAbove_rev_right {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
p.succAbove i.rev = (p.rev.succAbove i).rev
source
theorem Fin.rev_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
(p.succAbove i).rev = p.rev.succAbove i.rev

`rev` commutes with `succAbove`.

source
theorem Fin.predAbove_rev_left {n : ℕ} (p : Fin n) (i : Fin (n + 1)) :
p.rev.predAbove i = (p.predAbove i.rev).rev
source
theorem Fin.predAbove_rev_right {n : ℕ} (p : Fin n) (i : Fin (n + 1)) :
p.predAbove i.rev = (p.rev.predAbove i).rev
source
theorem Fin.rev_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) :
(p.predAbove i).rev = p.rev.predAbove i.rev

`rev` commutes with `predAbove`.

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