cycleType_cycleIcc_of_lt — Mathlib

English

If i < j, the cycleIcc(i,j) has cycle type { j − i + 1 }.

Русский

Если i < j, цикл cycleIcc(i,j) имеет тип цикла { j − i + 1 }.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i,j : \\mathrm{Fin}(n)},\\; i < j \\Rightarrow \\mathrm{cycleIcc}(i,j).\\mathrm{cycleType} = \\{ (j - i + 1) : \\mathbb{N} \\}$$$

Lean4

theorem cycleType_cycleIcc_of_lt (hij : i < j) : Perm.cycleType (cycleIcc i j) = {(j - i + 1 : ℕ)} := by
  simpa [le_of_lt hij, cycleType_cycleRange (castLT_sub_nezero hij)] using sub_val_of_le (le_of_lt hij)

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