exists_pow_eq — Mathlib

English

If f is a cycle and x,y are non-fixed, there exists a natural number i such that (f^i)(x) = y.

Русский

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

LaTeX

$$IsCycle(f) → f(x) ≠ x → f(y) ≠ y → ∃ i : ℕ, (f ^ i) x = y$$

Lean4

theorem exists_pow_eq (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℕ, (f ^ i) x = y :=
  by
  let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
  classical
    exact
    ⟨(n % orderOf f).toNat, by
      {
      have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
      rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]
    }⟩

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