cycleIcc_of_last

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.cycleIcc_of_last

English

If j < k, then (cycleIcc i j) k = k.

Русский

Если j < k, то (cycleIcc i j) k = k.

LaTeX

$$$cycleIcc(i,j)(k) = k \quad \text{если } j < k$$$

Lean4

theorem cycleIcc_of_last (hij : i ≤ j) [NeZero n] : (cycleIcc i j) j = i := by
  simp [cycleIcc_of_le_of_le hij (ge_of_eq rfl)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru