Hopf problem: pi 1 · threefold overlap mapping torus 2

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

theorem Mathoverflow1973.FundamentalGroupVanKampen.TwoOpenCover.inclusionHomU_surjective_of_overlapHomV_surjective {X : Type u_1} [TopologicalSpace X] (D : TwoOpenCover X) (hV : Function.Surjective ⇑D.overlapHomV) : Function.Surjective ⇑D.inclusionHomU