sameCycle_extendDomain — Mathlib

English

For finite α, if x and y lie in the same f-cycle, there exists an integer i with i < orderOf f such that (f^i) x = y.

Русский

Для конечного множества α, если x и y лежат в одном цикле f, существует целое i, i < orderOf f, такое что (f^i) x = y.

LaTeX

$$$[Finite\\ \\alpha]\\;\\forall f:\\mathrm{Equiv.Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\mathrm{SameCycle}(f,x,y) \\Rightarrow\\exists i\\in\\mathbb{Z}, i < \\mathrm{orderOf}(f) \\land (f^i)x = y.$$$

Lean4

@[simp]
theorem sameCycle_extendDomain {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
    SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y :=
  exists_congr fun n => by rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]

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