range_pow — Mathlib

English

If hs : f.IsCycleOn s and ha : a ∈ s, then the range of the map n ↦ (f^n)a over ℤ (or ℕ) equals s; i.e., the orbit of a under powers of f is exactly s.

Русский

Если f — цикл на s и a ∈ s, то орбита a под действием степеней f равна ровно s.

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \land a \in s \Rightarrow \mathrm{Range}(n \mapsto (f^n)a) = s$$$

Lean4

theorem range_pow (hs : s.Finite) (h : f.IsCycleOn s) (ha : a ∈ s) : Set.range (fun n => (f ^ n) a : ℕ → α) = s :=
  Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => h.1.mapsTo.perm_pow _ ha) fun _ => h.exists_pow_eq' hs ha

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