Mathlib.Data.Fin.Rev

Fin.rev_involutive theorem

: Involutive (rev : Fin n → Fin n)

Full source

theorem rev_involutive : Involutive (rev : Fin n → Fin n) := rev_rev

Involutivity of the Reverse Operation on Finite Types

Informal description

The reverse operation `rev` on the finite type `Fin n` is involutive, meaning that applying it twice returns the original element. That is, for any `i : Fin n`, we have $\text{rev}(\text{rev}(i)) = i$.

Fin.revPerm definition

: Equiv.Perm (Fin n)

Full source

/-- `Fin.rev` as an `Equiv.Perm`, the antitone involution `Fin n → Fin n` given by
`i ↦ n-(i+1)`. -/
@[simps! apply symm_apply]
def revPerm : Equiv.Perm (Fin n) :=
  Involutive.toPerm rev rev_involutive

Reverse permutation on finite types

Informal description

The permutation of the finite type `Fin n` given by the antitone involution $i \mapsto n - (i + 1)$, where $i$ is an element of `Fin n`.

Fin.rev_injective theorem

: Injective (@rev n)

Full source

theorem rev_injective : Injective (@rev n) :=
  rev_involutive.injective

Injectivity of the Reverse Operation on Finite Types

Informal description

The reverse operation $\text{rev} : \text{Fin } n \to \text{Fin } n$, defined by $\text{rev}(i) = n - 1 - i$, is injective. That is, for any $i, j \in \text{Fin } n$, if $\text{rev}(i) = \text{rev}(j)$, then $i = j$.

Fin.rev_surjective theorem

: Surjective (@rev n)

Full source

theorem rev_surjective : Surjective (@rev n) :=
  rev_involutive.surjective

Surjectivity of the Reverse Operation on Finite Types

Informal description

The reverse operation $\text{rev} : \text{Fin}\,n \to \text{Fin}\,n$, defined by $\text{rev}(i) = n - 1 - i$, is surjective. That is, for every $j \in \text{Fin}\,n$, there exists an $i \in \text{Fin}\,n$ such that $\text{rev}(i) = j$.

Fin.rev_bijective theorem

: Bijective (@rev n)

Full source

theorem rev_bijective : Bijective (@rev n) :=
  rev_involutive.bijective

Bijectivity of the Reverse Operation on Finite Types

Informal description

The reverse operation $\text{rev} : \text{Fin}\,n \to \text{Fin}\,n$, defined by $\text{rev}(i) = n - 1 - i$, is bijective. That is, it is both injective and surjective.

Fin.revPerm_symm theorem

: (@revPerm n).symm = revPerm

Full source

@[simp]
theorem revPerm_symm : (@revPerm n).symm = revPerm :=
  rfl

Reverse Permutation is an Involution on $\text{Fin}\,n$

Informal description

The reverse permutation on $\text{Fin}\,n$ is an involution, i.e., its inverse is itself. In symbols: $$ (\text{revPerm}_n)^{-1} = \text{revPerm}_n $$

Fin.cast_rev theorem

(i : Fin n) (h : n = m) : i.rev.cast h = (i.cast h).rev

Full source

theorem cast_rev (i : Fin n) (h : n = m) :
    i.rev.cast h = (i.cast h).rev := by
  subst h; simp

Commutativity of Cast and Reverse in Finite Types

Informal description

For any element $i$ in $\text{Fin}\,n$ and any equality $h : n = m$, the cast of the reverse of $i$ under $h$ is equal to the reverse of the cast of $i$ under $h$. In symbols: $$ \text{cast}_h(i^{\text{rev}}) = (\text{cast}_h(i))^{\text{rev}} $$

Fin.rev_eq_iff theorem

{i j : Fin n} : rev i = j ↔ i = rev j

Full source

theorem rev_eq_iff {i j : Fin n} : revrev i = j ↔ i = rev j := by
  rw [← rev_inj, rev_rev]

Reverse Equivalence in $\text{Fin}\,n$: $n-1-i = j \leftrightarrow i = n-1-j$

Informal description

For any elements $i, j$ in $\text{Fin}\,n$, the reverse of $i$ equals $j$ if and only if $i$ equals the reverse of $j$. In other words, $n - 1 - i = j \leftrightarrow i = n - 1 - j$.

Fin.rev_ne_iff theorem

{i j : Fin n} : rev i ≠ j ↔ i ≠ rev j

Full source

theorem rev_ne_iff {i j : Fin n} : revrev i ≠ jrev i ≠ j ↔ i ≠ rev j := rev_eq_iff.not

Reverse Inequality in $\text{Fin}\,n$: $\text{rev}(i) \neq j \leftrightarrow i \neq \text{rev}(j)$

Informal description

For any elements $i, j$ in $\text{Fin}\,n$, the reverse of $i$ is not equal to $j$ if and only if $i$ is not equal to the reverse of $j$. In other words, $n - 1 - i \neq j \leftrightarrow i \neq n - 1 - j$.

Fin.rev_lt_iff theorem

{i j : Fin n} : rev i < j ↔ rev j < i

Full source

theorem rev_lt_iff {i j : Fin n} : revrev i < j ↔ rev j < i := by
  rw [← rev_lt_rev, rev_rev]

Reverse Ordering in Finite Sets: $\text{rev}(i) < j \leftrightarrow \text{rev}(j) < i$

Informal description

For any two elements $i, j$ in $\text{Fin}\,n$, the reverse of $i$ is less than $j$ if and only if the reverse of $j$ is less than $i$. In other words, $\text{rev}(i) < j \leftrightarrow \text{rev}(j) < i$.

Fin.rev_le_iff theorem

{i j : Fin n} : rev i ≤ j ↔ rev j ≤ i

Full source

theorem rev_le_iff {i j : Fin n} : revrev i ≤ j ↔ rev j ≤ i := by
  rw [← rev_le_rev, rev_rev]

Inequality Characterization for the Reverse Operation on $\mathrm{Fin}\,n$

Informal description

For any two elements $i$ and $j$ in $\mathrm{Fin}\,n$, the inequality $\mathrm{rev}\,i \leq j$ holds if and only if $\mathrm{rev}\,j \leq i$, where $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.lt_rev_iff theorem

{i j : Fin n} : i < rev j ↔ j < rev i

Full source

theorem lt_rev_iff {i j : Fin n} : i < rev j ↔ j < rev i := by
  rw [← rev_lt_rev, rev_rev]

Reverse Order Inequality in Finite Type: $i < \text{rev}\,j \leftrightarrow j < \text{rev}\,i$

Informal description

For any elements $i$ and $j$ in $\text{Fin}\,n$, the inequality $i < \text{rev}\,j$ holds if and only if $j < \text{rev}\,i$, where $\text{rev}$ is the reverse operation on $\text{Fin}\,n$ defined by $\text{rev}\,k = n - 1 - k$.

Fin.le_rev_iff theorem

{i j : Fin n} : i ≤ rev j ↔ j ≤ rev i

Full source

theorem le_rev_iff {i j : Fin n} : i ≤ rev j ↔ j ≤ rev i := by
  rw [← rev_le_rev, rev_rev]

Reverse Ordering Relation in $\text{Fin}\,n$: $i \leq \text{rev}\,j \leftrightarrow j \leq \text{rev}\,i$

Informal description

For any two elements $i$ and $j$ in $\text{Fin}\,n$, the inequality $i \leq \text{rev}\,j$ holds if and only if $j \leq \text{rev}\,i$, where $\text{rev}$ is the reverse operation mapping $k$ to $n-1-k$.

Fin.val_rev_zero theorem

[NeZero n] : ((rev 0 : Fin n) : ℕ) = n.pred

Full source

@[simp] theorem val_rev_zero [NeZero n] : ((rev 0 : Fin n) : ℕ) = n.pred := rfl

Value of Reversed Zero in $\mathrm{Fin}\,n$ is $n-1$

Informal description

For any nonzero natural number $n$, the value of the reverse of $0$ in $\mathrm{Fin}\,n$ (as a natural number) is equal to the predecessor of $n$, i.e., $(\mathrm{rev}\,0 : \mathbb{N}) = n - 1$.

Fin.succAbove_rev_left theorem

(p : Fin (n + 1)) (i : Fin n) : p.rev.succAbove i = (p.succAbove i.rev).rev

Full source

lemma succAbove_rev_left (p : Fin (n + 1)) (i : Fin n) :
    p.rev.succAbove i = (p.succAbove i.rev).rev := by
  obtain h | h := (rev p).succ_le_or_le_castSucc i
  · rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
  · rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]

Reverse Commutation with $\mathrm{succAbove}$: Left Version

Informal description

For any element $p$ in $\mathrm{Fin}\,(n+1)$ and any element $i$ in $\mathrm{Fin}\,n$, the operation $\mathrm{succAbove}$ applied to the reverse of $p$ and $i$ is equal to the reverse of $\mathrm{succAbove}$ applied to $p$ and the reverse of $i$. In other words, \[ \mathrm{succAbove}\,(\mathrm{rev}\,p)\,i = \mathrm{rev}\,(\mathrm{succAbove}\,p\,(\mathrm{rev}\,i)). \] Here, $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.succAbove_rev_right theorem

(p : Fin (n + 1)) (i : Fin n) : p.succAbove i.rev = (p.rev.succAbove i).rev

Full source

lemma succAbove_rev_right (p : Fin (n + 1)) (i : Fin n) :
    p.succAbove i.rev = (p.rev.succAbove i).rev := by rw [succAbove_rev_left, rev_rev]

Reverse Commutation with $\mathrm{succAbove}$: Right Version

Informal description

For any element $p$ in $\mathrm{Fin}\,(n+1)$ and any element $i$ in $\mathrm{Fin}\,n$, the operation $\mathrm{succAbove}$ applied to $p$ and the reverse of $i$ is equal to the reverse of $\mathrm{succAbove}$ applied to the reverse of $p$ and $i$. In other words, \[ \mathrm{succAbove}\,p\,(\mathrm{rev}\,i) = \mathrm{rev}\,(\mathrm{succAbove}\,(\mathrm{rev}\,p)\,i). \] Here, $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.rev_succAbove theorem

(p : Fin (n + 1)) (i : Fin n) : rev (succAbove p i) = succAbove (rev p) (rev i)

Full source

/-- `rev` commutes with `succAbove`. -/
lemma rev_succAbove (p : Fin (n + 1)) (i : Fin n) :
    rev (succAbove p i) = succAbove (rev p) (rev i) := by
  rw [succAbove_rev_left, rev_rev]

Reverse Commutation with $\mathrm{succAbove}$: Symmetric Version

Informal description

For any element $p$ in $\mathrm{Fin}\,(n+1)$ and any element $i$ in $\mathrm{Fin}\,n$, the reverse of the $\mathrm{succAbove}$ operation applied to $p$ and $i$ is equal to the $\mathrm{succAbove}$ operation applied to the reverse of $p$ and the reverse of $i$. In other words, \[ \mathrm{rev}\,(\mathrm{succAbove}\,p\,i) = \mathrm{succAbove}\,(\mathrm{rev}\,p)\,(\mathrm{rev}\,i). \] Here, $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.predAbove_rev_left theorem

(p : Fin n) (i : Fin (n + 1)) : p.rev.predAbove i = (p.predAbove i.rev).rev

Full source

lemma predAbove_rev_left (p : Fin n) (i : Fin (n + 1)) :
    p.rev.predAbove i = (p.predAbove i.rev).rev := by
  obtain h | h := (rev i).succ_le_or_le_castSucc p
  · rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
  · rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

Reverse Commutation with $\mathrm{predAbove}$: Left Version

Informal description

For any element $p$ in $\mathrm{Fin}\,n$ and any element $i$ in $\mathrm{Fin}\,(n+1)$, applying the $\mathrm{predAbove}$ operation to the reverse of $p$ and $i$ is equal to the reverse of applying $\mathrm{predAbove}$ to $p$ and the reverse of $i$. In other words, \[ \mathrm{predAbove}\,(\mathrm{rev}\,p)\,i = \mathrm{rev}\,(\mathrm{predAbove}\,p\,(\mathrm{rev}\,i)). \] Here, $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.predAbove_rev_right theorem

(p : Fin n) (i : Fin (n + 1)) : p.predAbove i.rev = (p.rev.predAbove i).rev

Full source

lemma 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]

Reverse Commutation with $\mathrm{predAbove}$: Right Version

Informal description

For any element $p$ in $\mathrm{Fin}\,n$ and any element $i$ in $\mathrm{Fin}\,(n+1)$, applying the $\mathrm{predAbove}$ operation to $p$ and the reverse of $i$ is equal to the reverse of applying $\mathrm{predAbove}$ to the reverse of $p$ and $i$. In other words, \[ \mathrm{predAbove}\,p\,(\mathrm{rev}\,i) = \mathrm{rev}\,(\mathrm{predAbove}\,(\mathrm{rev}\,p)\,i). \] Here, $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.rev_predAbove theorem

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

Full source

/-- `rev` commutes with `predAbove`. -/
lemma 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]

Reverse Commutes with $\mathrm{predAbove}$

Informal description

For any natural number $n$, element $p \in \mathrm{Fin}\,n$, and element $i \in \mathrm{Fin}\,(n+1)$, the reverse of $\mathrm{predAbove}\,p\,i$ equals $\mathrm{predAbove}\,(\mathrm{rev}\,p)\,(\mathrm{rev}\,i)$. In other words, \[ \mathrm{rev}(\mathrm{predAbove}\,p\,i) = \mathrm{predAbove}\,(\mathrm{rev}\,p)\,(\mathrm{rev}\,i), \] where $\mathrm{rev}\,k = n - 1 - k$ for any $k \in \mathrm{Fin}\,n$.

Fin.add_rev_cast theorem

(j : Fin (n + 1)) : j.1 + j.rev.1 = n

Full source

lemma add_rev_cast (j : Fin (n+1)) : j.1 + j.rev.1 = n := by
  obtain ⟨j, hj⟩ := j
  simp [Nat.add_sub_cancel' <| le_of_lt_succ hj]

Sum of Fin Element and Its Reverse Equals $n$

Informal description

For any element $j$ of $\text{Fin}(n+1)$, the sum of the value of $j$ and its reverse $\text{rev}(j)$ is equal to $n$. That is, $j + \text{rev}(j) = n$.

Fin.rev_add_cast theorem

(j : Fin (n + 1)) : j.rev.1 + j.1 = n

Full source

lemma rev_add_cast (j : Fin (n+1)) : j.rev.1 + j.1 = n := by
  rw [Nat.add_comm, j.add_rev_cast]

Sum of Reverse and Original Fin Element Equals $n$

Informal description

For any element $j$ of $\text{Fin}(n+1)$, the sum of the value of its reverse $\text{rev}(j)$ and $j$ is equal to $n$. That is, $\text{rev}(j) + j = n$.

Definitions