cycleRange_of_gt

Mathlib.GroupTheory.Perm.Fin

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

English

If i < j, then (cycleRange(i))(j) = j, i.e., j is fixed by the cycleRange from i.

Русский

Если i < j, то (cycleRange(i))(j) = j, то есть j зафиксирован циклRange от i.

LaTeX

$$$ (\\mathrm{cycleRange}(i))(j) = j \\quad \\text{если } i

Lean4

theorem cycleRange_of_gt (h : i < j) : cycleRange i j = j :=
  by
  rw [cycleRange, Perm.extendDomain_apply_not_subtype]
  simpa using h

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

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

Разделы

Аффилиация

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