Hopf problem: recognition · smale 7

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

theorem Mathoverflow1973.Smale.DiskFraming.exists_nonzero_smooth_curve_with_endpoint_germs {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] [FiniteDimensional ℝ B] {a b : ℝ → B} {U V : Set ℝ} (ha : ContDiffOn ℝ (↑⊤) a U) (hb : ContDiffOn ℝ (↑⊤) b V) (hU : IsOpen U) (hV : IsOpen V) (h0U : 0 ∈ U) (h1V : 1 ∈ V) (ha0 : a 0 ≠ 0) (hb1 : b 1 ≠ 0) (hdim : 2 ≤ Module.finrank ℝ B) : ∃ (v : ℝ → B), ContDiff ℝ (↑⊤) v ∧ (∀ (t : ℝ), v t ≠ 0) ∧ v =ᶠ[nhds 0] a ∧ v =ᶠ[nhds 1] b