Hopf problem: foundations · line bundle transport

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

theorem Mathoverflow1973.LineBundleTransport.exists_interval_cutoff (a b : ℝ) : ∃ (χ : ℝ → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ Set.EqOn χ (fun (x : ℝ) => 1) (Set.uIcc a b)