∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b : α}
  [inst_3 : Fact (a ≤ b)] {E : Type u_2} [inst_4 : TopologicalSpace E] (f : C(↑(Set.Icc a b), E)),
  Continuous ⇑(ContinuousMap.IccExtendCM f)