mathlib

bbca2890 - feat(dynamics/periodic_pts): `chain.pairwise` on orbit (#12991)

feat(dynamics/periodic_pts): `chain.pairwise` on orbit (#12991) We prove that a relation holds pairwise on an orbit iff it does for `f^[n] x` and `f^[n+1] x` for any `n`.