Finite forward orbits of injective maps

An injective self-map cannot have a finite forward orbit with a nonperiodic initial point. The injectivity hypothesis is what lets us cancel the transient part of a repeated pair of iterates.

theorem BGS.exists_positive_iterate_eq_self_of_finite_forwardOrbit {X : Type u} {f : X → X} {x : X} (hf : Function.Injective f) (horbit : (Set.range fun (n : ℕ) => f^[n] x).Finite) : ∃ (n : ℕ), 0 < n ∧ f^[n] x = x

If the forward orbit of x under an injective self-map is finite, then a positive iterate returns to x.

theorem BGS.exists_positive_iterate_eq_self_of_forwardOrbit_subset {X : Type u} {f : X → X} {x : X} (hf : Function.Injective f) {s : Set X} (hs : s.Finite) (horbit : (Set.range fun (n : ℕ) => f^[n] x) ⊆ s) : ∃ (n : ℕ), 0 < n ∧ f^[n] x = x

A finite set containing every forward iterate forces a positive return for an injective self-map. This form is convenient when an orbit has already been bounded by a concrete finite set.