Connecting orbits of a real flow

A periodic orbit with a forward or backward limit is constant. A nonconstant orbit with either limit is therefore injectively parametrized by time. In particular, an orbit connecting distinct backward and forward limits has the freeness needed to divide parametrized Morse trajectories by time translation when constructing their moduli spaces.

The argument uses only continuity of the flow and uniqueness of limits, so it also applies to connecting trajectories in other dynamical systems. The trajectory-space interpretation follows M. Audin and M. Damian, Morse Theory and Floer Homology, Springer, 2014, Chapter 2.

theorem Flow.orbit_injective_of_ne_of_mem_unstableSet_inter_stableSet {α : Type u_1} [TopologicalSpace α] [T1Space α] {φ : Flow ℝ α} {p q x : α} (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : Function.Injective fun (t : ℝ) => φ.toFun t x

An orbit connecting distinct backward and forward limits has a free time parameter.