support_cycleOf_eq_nil_iff

Mathlib.GroupTheory.Perm.Cycle.Factors

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.support_cycleOf_eq_nil_iff

English

For any f and x, the cycleOf x support is empty iff x is fixed by f.

Русский

Для любой f и x поддержка cycleOf x пустая тогда и только тогда, когда x зафиксирован f.

LaTeX

$$$(f\\\\.cycleOf x).\\\\support = \\\\emptyset \\\\iff x \\\\in f\\\\.support^c$$$

Lean4

theorem support_cycleOf_eq_nil_iff [DecidableEq α] [Fintype α] : (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp

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

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

Разделы

Аффилиация

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