support_cycleOf_le — Mathlib

English

For any SameCycle relation between x and y, there exists a positive exponent i bounded by the cycle length such that f^i x = y.

Русский

Для любых x,y в SameCycle существует положительная степнь i, ограниченная длиной цикла, такая что f^i x = y.

LaTeX

$$$f.SameCycle x y \\\\Rightarrow \\\\exists i \\\\in \\\\mathbb{N}, 0 < i \\\\land i \\\\le #(f.cycleOf x).\\\\support + 1 \\\\land (f^i) x = y$$$

Lean4

theorem support_cycleOf_le [DecidableEq α] [Fintype α] (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f :=
  by
  intro y hy
  rw [mem_support, cycleOf_apply] at hy
  split_ifs at hy
  · exact mem_support.mpr hy
  · exact absurd rfl hy

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