Hopf problem: pi 1 · fundamental group van kampen 2

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

theorem Mathoverflow1973.FundamentalGroupVanKampen.convexComb_mem_Icc {s t u v : ↑unitInterval} (hu : u ∈ Set.Icc s t) (hv : v ∈ Set.Icc s t) (r : ↑unitInterval) : Set.Icc.convexComb u v r ∈ Set.Icc s t