Hopf problem: recognition · degree 1 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Degree.FlowCancellation.exists_level_crossing_of_endpoint_limits
{X : Type u_1}
[TopologicalSpace X]
(F : Flow ℝ X)
{f : X → ℝ}
(hf : Continuous f)
{x p q : X}
(hp : Filter.Tendsto (fun (t : ℝ) => F.toFun t x) Filter.atBot (nhds p))
(hq : Filter.Tendsto (fun (t : ℝ) => F.toFun t x) Filter.atTop (nhds q))
{c : ℝ}
(hpc : c < f p)
(hqc : f q < c)
: