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)

theorem Fin.rev_involutive {n : ℕ} : Function.Involutive rev

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 ⋯

@[simp]

theorem Fin.revPerm_apply {n : ℕ} (i : Fin n) : revPerm i = i.rev

@[simp]

theorem Fin.revPerm_symm_apply {n : ℕ} (i : Fin n) : (Equiv.symm revPerm) i = i.rev

theorem Fin.rev_injective {n : ℕ} : Function.Injective rev

theorem Fin.rev_surjective {n : ℕ} : Function.Surjective rev

theorem Fin.rev_bijective {n : ℕ} : Function.Bijective rev

@[simp]

theorem Fin.revPerm_symm {n : ℕ} : Equiv.symm revPerm = revPerm

theorem Fin.cast_rev {n m : ℕ} (i : Fin n) (h : n = m) : Fin.cast h i.rev = (Fin.cast h i).rev

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

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) : p.rev.succAbove i = (p.succAbove i.rev).rev

theorem Fin.succAbove_rev_right {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i.rev = (p.rev.succAbove i).rev

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.

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

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

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.

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