Hopf problem: recognition · smale 11

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

theorem Mathoverflow1973.Smale.CoverNaturality.map_intersection {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (U V : Set X) (U' V' : Set Y) (f : C(X, Y)) (hU : Set.MapsTo (⇑f) U U') (hV : Set.MapsTo (⇑f) V V') : Set.MapsTo (⇑f) (U ∩ V) (U' ∩ V')