Hopf problem: recognition · degree 2

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

theorem Mathoverflow1973.Degree.FlowSuspension.whole_level_basins_of_holonomy {X : Type u_1} {M : Type u_2} [TopologicalSpace M] (F H G : Flow ℝ M) (ι : X → M) (D : X → X) (hHtop : ∀ (x p : M), Filter.Tendsto (fun (t : ℝ) => H.toFun t x) Filter.atTop (nhds p) ↔ Filter.Tendsto (fun (t : ℝ) => F.toFun t x) Filter.atTop (nhds p)) (hHbot : ∀ (x p : M), Filter.Tendsto (fun (t : ℝ) => H.toFun t x) Filter.atBot (nhds p) ↔ Filter.Tendsto (fun (t : ℝ) => F.toFun t x) Filter.atBot (nhds p)) (hend : ∀ (x : X), G.toFun 1 (ι x) = H.toFun 1 (ι (D x))) (hleft : ∀ (x : X), ∀ t ≤ 0, G.toFun t (ι x) = H.toFun t (ι x)) (hright : ∀ (x : X) (t : ℝ), 0 ≤ t → G.toFun t (H.toFun 1 (ι x)) = H.toFun t (H.toFun 1 (ι x))) : (∀ (x : X) (p : M), Filter.Tendsto (fun (t : ℝ) => G.toFun t (ι x)) Filter.atBot (nhds p) ↔ Filter.Tendsto (fun (t : ℝ) => F.toFun t (ι x)) Filter.atBot (nhds p)) ∧ ∀ (x : X) (p : M), Filter.Tendsto (fun (t : ℝ) => G.toFun t (ι x)) Filter.atTop (nhds p) ↔ Filter.Tendsto (fun (t : ℝ) => F.toFun t (ι (D x))) Filter.atTop (nhds p)