isCycle_cycleOf_iff — Mathlib

English

For any permutation f and any x, the cycle of x is nontrivial exactly when x is moved by f.

Русский

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

LaTeX

$$$\\\\forall f \\\\forall x, IsCycle\\\\(cycleOf f x) \\\\iff f(x) \\\\neq x$$$

Lean4

/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
theorem isCycle_cycleOf_iff (f : Perm α) [DecidableRel f.SameCycle] : IsCycle (cycleOf f x) ↔ f x ≠ x :=
  by
  refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩
  rw [Ne, ← cycleOf_eq_one_iff f]
  exact hx.ne_one

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