src/HOL/Topological_Spaces.thy
changeset 61426 d53db136e8fd
parent 61342 b98cd131e2b5
child 61520 8f85bb443d33
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Oct 13 09:21:21 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Oct 13 12:42:08 2015 +0100
     1.3 @@ -1393,11 +1393,15 @@
     1.4    unfolding continuous_on_closed_invariant
     1.5    by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
     1.6  
     1.7 +corollary closed_vimage_Int[continuous_intros]:
     1.8 +  assumes "closed s" and "continuous_on t f" and t: "closed t"
     1.9 +  shows "closed (f -` s \<inter> t)"
    1.10 +  using assms unfolding continuous_on_closed_vimage [OF t]  by simp
    1.11 +
    1.12  corollary closed_vimage[continuous_intros]:
    1.13    assumes "closed s" and "continuous_on UNIV f"
    1.14    shows "closed (f -` s)"
    1.15 -  using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
    1.16 -  by simp
    1.17 +  using closed_vimage_Int [OF assms] by simp
    1.18  
    1.19  lemma continuous_on_open_Union:
    1.20    "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"