isCycle_cycleIcc — Mathlib

English

If i < j, then the permutation cycleIcc(i,j) is a cycle.

Русский

Если i < j, то перестановка cycleIcc(i,j) является циклом.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i,j : \\mathrm{Fin}(n)},\\; i < j \\Rightarrow (\\mathrm{cycleIcc}(i,j)).IsCycle$$$

Lean4

theorem isCycle_cycleIcc (hij : i < j) : (cycleIcc i j).IsCycle := by
  simpa [le_of_lt hij] using
    Equiv.Perm.IsCycle.extendDomain (natAdd_castLEEmb _).toEquivRange (isCycle_cycleRange (castLT_sub_nezero hij))

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