exists_pow_eq_of_mem_support — Mathlib

English

If f and x,y are in the same cycle and x is in the support of f, there exists a power of f sending x to y with an exponent bounded by the cycle length.

Русский

Если x,y в одной цепи f и x лежит в поддержке f, существует степень f, переводящая x в y, с ограничением по длине цикла.

LaTeX

$$$h : SameCycle f x y \\\\land hx : x \\\\in f\\\\.support \\\\Rightarrow \\\\exists i < #(f.cycleOf x).\\\\support, (f^i) x = y$$$

Lean4

theorem exists_pow_eq_of_mem_support {f} [DecidableEq α] [Fintype α] (h : SameCycle f x y) (hx : x ∈ f.support) :
    ∃ i < #(f.cycleOf x).support, (f ^ i) x = y :=
  h.exists_pow_eq_of_mem_support_aux hx

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