SameCycle — Mathlib

English

Two points x and y are in the same cycle of a permutation f if and only if there exists an integer i with f^i(x) = y.

Русский

Точки x и y лежат в одной и той же циклической компоненте перестановки f, если существует целое i такое, что f^i(x) = y.

LaTeX

$$def SameCycle (f : Perm α) (x y : α) : Prop := ∃ i : ℤ, (f ^ i) x = y$$

Lean4

/-- The equivalence relation indicating that two points are in the same cycle of a permutation. -/
def SameCycle (f : Perm α) (x y : α) : Prop :=
  ∃ i : ℤ, (f ^ i) x = y

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