Hopf problem: recognition · smale 4

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.MorseCancel.flow_time_atTop_limit_iff {M : Type u_1} [TopologicalSpace M] (F : Flow ℝ M) (d : ℝ) (x p : M) : Filter.Tendsto (fun (t : ℝ) => F.toFun t (F.toFun d x)) Filter.atTop (nhds p) ↔ Filter.Tendsto (fun (t : ℝ) => F.toFun t x) Filter.atTop (nhds p)