isCycle_iff_sameCycle — Mathlib

English

If f is a permutation and x ≠ f(x), then IsCycle f is equivalent to: for all y, SameCycle f x y if and only if f(y) ≠ y.

Русский

Если f — перестановка и x ≠ f(x), то IsCycle f эквивалентно: для любого y, SameCycle f x y тогда и только тогда, когда f(y) ≠ y.

LaTeX

$$isCycle_iff_sameCycle (hx : f x ≠ x) : IsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y$$

Lean4

theorem isCycle_iff_sameCycle (hx : f x ≠ x) : IsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y :=
  ⟨fun hf y =>
    ⟨fun ⟨i, hi⟩ hy =>
      hx <| by
        rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
        rw [hi, hy],
      hf.exists_zpow_eq hx⟩,
    fun h => ⟨x, hx, fun _ hy => h.2 hy⟩⟩

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