exists_zpow_eq — Mathlib

English

If f is a cycle and x,y are non-fixed, there exists an integer i with f^i(x) = y, i.e., x and y lie in the same cycle.

Русский

Если f — цикл и x, y не зафиксированы, существует целое i такое, что f^i(x) = y, то есть x и y лежат в одном цикле.

LaTeX

$$IsCycle(f) → f(x) ≠ x → f(y) ≠ y → ∃ i ∈ \mathbb{Z}, f^i(x) = y$$

Lean4

theorem exists_zpow_eq : IsCycle f → f x ≠ x → f y ≠ y → ∃ i : ℤ, (f ^ i) x = y :=
  IsCycle.sameCycle

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