src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

   finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
 qed
 
 lemma closed_unit_cube: "closed unit_cube"
   unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
-  by (rule closed_INT, auto intro!: closed_Collect_le)
+  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
 
 lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
   unfolding compact_eq_seq_compact_metric
   using bounded_unit_cube closed_unit_cube
   by (rule bounded_closed_imp_seq_compact)

   let ?U = "unit_cube :: 'a set"
   have "\<Sum>Basis /\<^sub>R 2 \<in> interior ?U"
   proof (rule interiorI)
     let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
     show "open ?I"
-      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less)
+      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
     show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
       by simp
     show "?I \<subseteq> unit_cube"
       unfolding unit_cube_def by force
   qed