cycleRange — Mathlib

English

cycleRange(i) is the permutation that cycles the block 0,1,...,i and fixes i+1,...,n-1.

Русский

cycleRange(i) — перестановка, которая циклирует 0,1,...,i и фиксирует i+1,...,n-1.

LaTeX

$$$ \\mathrm{cycleRange}(i) \\in \\mathrm{Perm}(\\mathrm{Fin}(n)) \\quad\\text{и}{\\ }\\text{циклично переставляет }(0,1,\\dots,i) \\text{, оставляя} (i+1,...,n-1) \\\\text{неизменными}$$$

Lean4

/-- `Fin.cycleRange i` is the cycle `(0 1 2 ... i)` leaving `(i+1 ... (n-1))` unchanged. -/
def cycleRange {n : ℕ} (i : Fin n) : Perm (Fin n) :=
  (finRotate (i + 1)).extendDomain (castLEEmb (by cutsat)).toEquivRange

Похожие утверждения