Hopf problem: recognition · smale 3

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

theorem Mathoverflow1973.Smale.DiskFraming.exists_pos_prod_closedBall_subset {D : Type u_1} {Z : Type u_2} [TopologicalSpace D] [NormedAddCommGroup Z] {K : Set D} {U : Set (D × Z)} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ×ˢ {0} ⊆ U) : ∃ (ε : ℝ), 0 < ε ∧ K ×ˢ Metric.closedBall 0 ε ⊆ U