cycleType_cycleIcc_of_ge — Mathlib

English

If i ≤ j, the cycleIcc(j,i) has cycle type ∅ (empty).

Русский

Если i ≤ j, цикл cycleIcc(j,i) разлагается на ноль циклов (пустой цикл).

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i,j : \\mathrm{Fin}(n)},\\; i \\le j \\Rightarrow \\mathrm{cycleIcc}(j,i).\\mathrm{cycleType} = \\emptyset$$$

Lean4

theorem cycleType_cycleIcc_of_ge (hij : i ≤ j) [NeZero n] : Perm.cycleType (cycleIcc j i) = ∅ := by
  simpa using cycleIcc_ge hij

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