range_zpow — Mathlib

English

Similarly, the range of the map n ↦ (f^n)a over n ∈ ℤ equals s when f is cycle-on s.

Русский

То же самое для целочисленных степеней: множество значений { (f^n)a : n ∈ ℤ } равно s.

LaTeX

$$$\mathrm{IsCycleOn}(f,s) \Rightarrow \mathrm{Range}\bigl(n \mapsto (f^n)a : \mathbb{Z} \to \alpha\bigr) = s$$$

Lean4

theorem range_zpow (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.perm_zpow _).mapsTo ha) <| h.2 ha

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