Hopf problem: hurewicz · third hurewicz

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

theorem Mathoverflow1973.ThirdHurewicz.nativeInterval_convexComb_mul (a b t : ↑unitInterval) : Set.Icc.convexComb (a * b) a t = a * Set.Icc.convexComb b 1 t