cycleRange_apply — Mathlib

English

For all i,j, the image of j under cycleRange(i) is given by a piecewise rule: j+1 if j<i, 0 if j=i, and j otherwise.

Русский

Для всех i,j образ j под cycleRange(i) задаётся по правилу: j+1 при j<i, 0 при j=i, иначе j.

LaTeX

$$$ \\mathrm{cycleRange}(i)(j) = \\begin{cases} j+1, & j

Lean4

theorem cycleRange_apply [NeZero n] (i j : Fin n) : cycleRange i j = if j < i then j + 1 else if j = i then 0 else j := by split_ifs with h₁ h₂ · exact cycleRange_of_lt h₁ · exact cycleRange_of_eq h₂ · exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

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