In this file we prove that the projection set.proj_Icc f a b h is a quotient map, and use it
to show that Icc_extend h f is continuous if and only if f is continuous.
set.proj_Icc f a b h
Icc_extend h f
See Note [continuity lemma statement].
A useful special case of continuous.Icc_extend.