Hopf problem: recognition · smale 1

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

theorem Mathoverflow1973.Smale.MorsePerturbation.isOpen_forall_mem_compact {P : Type u_1} {X : Type u_2} [TopologicalSpace P] [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {U : Set (P × X)} (hU : IsOpen U) : IsOpen {p : P | ∀ x ∈ K, (p, x) ∈ U}