sameCycle — Mathlib

English

If f is an IsCycle, then two non-fixed points x and y lie on the same cycle of f.

Русский

Если f — цикл, то любые две несдвинутые точки x и y лежат на одном и том же цикле f.

LaTeX

$$IsCycle(f) ∧ f(x) ≠ x ∧ f(y) ≠ y → SameCycle(f, x, y)$$

Lean4

protected theorem sameCycle (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) : SameCycle f x y :=
  let ⟨g, hg⟩ := hf
  let ⟨a, ha⟩ := hg.2 hx
  let ⟨b, hb⟩ := hg.2 hy
  ⟨b - a, by rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]⟩

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