finRotate_succ_apply
theorem finRotate_succ_apply : ∀ {n : ℕ} (i : Fin (n + 1)), (finRotate (n + 1)) i = i + 1
This theorem states that, for any natural number `n` and any value `i` in the finite set `Fin (n + 1)`, applying the function `finRotate (n + 1)` to `i` results in `i` incremented by 1. In other words, the `finRotate` function effectively rotates or shifts the elements in the finite set to the right by one step.
More concisely: For any natural number `n` and `i` in `Fin (n + 1)`, `finRotate (n + 1) i = i.succ`.
|
finSuccEquiv_succ
theorem finSuccEquiv_succ : ∀ {n : ℕ} (m : Fin n), (finSuccEquiv n) m.succ = some m
This theorem states that for any natural number `n` and any value `m` in the finite sequence `Fin n`, applying the function `Fin.succ` to `m` and then the equivalence function `finSuccEquiv n` will yield `some m`. In other words, it asserts that the `finSuccEquiv n` function correctly identifies the successor of a `Fin n` value as its equivalent in the `Option (Fin n)` set. This is essentially a form of mapping between a finite set of size `n+1` and an optional finite set of size `n`.
More concisely: For any natural number `n` and `Fin n` value `m`, `Fin.succ m = some (finSuccEquiv n m)`.
|
finSuccEquiv'_zero
theorem finSuccEquiv'_zero : ∀ {n : ℕ}, finSuccEquiv' 0 = finSuccEquiv n
This theorem, `finSuccEquiv'_zero`, states that for all natural numbers `n`, the equivalence `finSuccEquiv' 0` is equal to `finSuccEquiv n`. Here, `finSuccEquiv' 0` is an equivalence that removes the zeroth element from the finite set `Fin (n + 1)` and maps it to `none`, creating an `Option (Fin n)`. The `finSuccEquiv n` is an equivalence between `Fin (n + 1)` and `Option (Fin n)`. Thus, the theorem asserts that these two operations of creating an option type by removing the zeroth element are equivalent.
More concisely: For all natural numbers `n`, the equivalence `finSuccEquiv' 0` on `Fin (n + 1)` equals the equivalence `finSuccEquiv n` between `Fin (n + 1)` and `Option (Fin n)`.
|
finSuccEquiv'_succAbove
theorem finSuccEquiv'_succAbove : ∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), (finSuccEquiv' i) (i.succAbove j) = some j
The theorem `finSuccEquiv'_succAbove` states that for any natural number `n`, and for any `i` selected from the finite set `Fin (n + 1)` and `j` selected from the finite set `Fin n`, when we apply the function `finSuccEquiv'` with `i` to the result of `Fin.succAbove` with `i` and `j`, we always get `some j`. In other words, the function `finSuccEquiv'` applied to `Fin.succAbove i j` always gives `some j`. Here, `finSuccEquiv'` is an equivalence that removes the element `i` and maps it to `none`, while `Fin.succAbove` is a function that embeds `Fin n` into `Fin (n + 1)` with a hole around `i`.
More concisely: For any natural numbers `n`, `i` in `Fin (n + 1)`, and `j` in `Fin n`, applying the function `finSuccEquiv'` to the result of `Fin.succAbove i j` always returns `some j`.
|
finSuccEquiv_symm_some
theorem finSuccEquiv_symm_some : ∀ {n : ℕ} (m : Fin n), (finSuccEquiv n).symm (some m) = m.succ
The theorem `finSuccEquiv_symm_some` states that for all natural numbers `n` and for all `m` in `Fin n`, the inverse of the equivalence `finSuccEquiv n`, when applied to `m` wrapped in `some`, is equal to the successor of `m` in `Fin (Nat.succ n)`. In simpler terms, using the inverse equivalence `finSuccEquiv n` to convert an optional finite number back to a finite number increments the value by one.
More concisely: For all natural numbers `n` and `m` in `Fin n`, the inverse of `finSuccEquiv n` applied to `some m` equals `some (m.succ)` in `Fin (Nat.succ n)`.
|