equal
deleted
inserted
replaced
488 using * \<open>J \<subseteq> I\<close> by auto |
488 using * \<open>J \<subseteq> I\<close> by auto |
489 also have "openin T1 (...)" |
489 also have "openin T1 (...)" |
490 using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast |
490 using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast |
491 ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp |
491 ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp |
492 next |
492 next |
493 have "f ` topspace T1 \<subseteq> topspace (product_topology T I)" |
493 have "f \<in> topspace T1 \<rightarrow> topspace (product_topology T I)" |
494 using assms continuous_map_def by fastforce |
494 using assms continuous_map_funspace by (force simp: Pi_iff) |
495 then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}" |
495 then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}" |
496 by (simp add: product_topology_def) |
496 by (fastforce simp add: product_topology_def Pi_iff) |
497 qed |
497 qed |
498 |
498 |
499 lemma continuous_map_product_then_coordinatewise [intro]: |
499 lemma continuous_map_product_then_coordinatewise [intro]: |
500 assumes "continuous_map T1 (product_topology T I) f" |
500 assumes "continuous_map T1 (product_topology T I) f" |
501 shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)" |
501 shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)" |