Fin.cycleRange_of_le
theorem Fin.cycleRange_of_le : ∀ {n : ℕ} {i j : Fin n.succ}, j ≤ i → i.cycleRange j = if j = i then 0 else j + 1 := by
sorry
The theorem `Fin.cycleRange_of_le` states that for any natural number `n` and for any two elements `i` and `j` of the finite set `Fin (Nat.succ n)`, if `j` is less than or equal to `i`, then the result of applying the `cycleRange` function to `i` and then applying the resulting permutation to `j` is equal to `0` if `j` equals `i`, otherwise it is equal to `j + 1`. Here, the `cycleRange` function is defined as rotating the indices from `0` up to `i`, leaving the rest unchanged.
More concisely: For any natural number `n` and `i`, `j` in `Fin (Nat.succ n)`, if `j ≤ i`, then `cycleRange i j = if j = i then 0 else j + 1`.
|
Fin.cycleRange_of_gt
theorem Fin.cycleRange_of_gt : ∀ {n : ℕ} {i j : Fin n.succ}, i < j → i.cycleRange j = j
The theorem `Fin.cycleRange_of_gt` states that for any natural number `n` and any two finite numbers `i` and `j` within the range `0` to `n+1`, if `i` is less than `j`, then applying the `Fin.cycleRange` function to `i` and then applying the resulting permutation to `j` results in `j` itself. In other words, if `i` is less than `j`, `j` is left unchanged by the permutation generated by `Fin.cycleRange i`.
More concisely: For all natural numbers n, if i < j in the range 0 to n+1, then applying the permutation obtained from Fin.cycleRange i leaves j unchanged.
|
Finset.univ_perm_fin_succ
theorem Finset.univ_perm_fin_succ :
∀ {n : ℕ}, Finset.univ = Finset.map Equiv.Perm.decomposeFin.symm.toEmbedding Finset.univ
This theorem states that for any natural number `n`, the set of all permutations of `Fin (n + 1)` is obtained by mapping the set of all permutations of `Fin n` through the inverse of the `Equiv.Perm.decomposeFin` function, which decomposes a permutation of `Fin (n + 1)` into a fixed element and a permutation of the remaining `Fin n` elements. In other words, any permutation of `Fin (n + 1)` can be constructed by picking an element from `Fin (n + 1)` and a permutation of `Fin n`, and the set of all such combinations constitutes the entire set of permutations of `Fin (n + 1)`.
More concisely: The set of permutations of Fin (n+1) is equivalent to the cartesian product of Fin (n+1) with the set of permutations of Fin n.
|