IsCycle — Mathlib

English

A cycle is a nontrivial permutation in which every pair of non-fixed points lie on the same cycle of the permutation.

Русский

Цикл — это нетривиальная перестановка, в которой любые две нефиксирующие точки лежат в одном цикле перестановки.

LaTeX

$$IsCycle(f) is defined by: ∃ x, f(x) ≠ x ∧ ∀ y, f(y) ≠ y → SameCycle(f, x, y).$$

Lean4

/-- A cycle is a non-identity permutation where any two nonfixed points of the permutation are
related by repeated application of the permutation. -/
def IsCycle (f : Perm α) : Prop :=
  ∃ x, f x ≠ x ∧ ∀ ⦃y⦄, f y ≠ y → SameCycle f x y

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