Hopf problem: cusp fibre · cusp positive retraction

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

theorem Mathoverflow1973.CuspRetraction.Patching.exists_positive_sublevel_subset_open {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) (hf : ∀ (x : X), 0 ≤ f x) {r : ℝ} (hr : 0 < r) (hc : IsCompact {x : X | f x ≤ r}) {U : Set X} (hU : IsOpen U) (hS : {x : X | f x = 0} ⊆ U) : ∃ (η : ℝ), 0 < η ∧ η ≤ r ∧ {x : X | f x ≤ η} ⊆ U