src/HOL/Library/Product_Vector.thy
changeset 51478 270b21f3ae0a
parent 51002 496013a6eb38
child 51642 400ec5ae7f8f
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -117,15 +117,6 @@
     1.4      by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
     1.5  qed
     1.6  
     1.7 -lemma openI: (* TODO: move *)
     1.8 -  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
     1.9 -  shows "open S"
    1.10 -proof -
    1.11 -  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
    1.12 -  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
    1.13 -  ultimately show "open S" by simp
    1.14 -qed
    1.15 -
    1.16  lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
    1.17    unfolding image_def subset_eq by force
    1.18  
    1.19 @@ -202,15 +193,23 @@
    1.20         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
    1.21  qed
    1.22  
    1.23 +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
    1.24 +  unfolding continuous_def by (rule tendsto_fst)
    1.25 +
    1.26 +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
    1.27 +  unfolding continuous_def by (rule tendsto_snd)
    1.28 +
    1.29 +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
    1.30 +  unfolding continuous_def by (rule tendsto_Pair)
    1.31 +
    1.32  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
    1.33 -  unfolding isCont_def by (rule tendsto_fst)
    1.34 +  by (fact continuous_fst)
    1.35  
    1.36  lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
    1.37 -  unfolding isCont_def by (rule tendsto_snd)
    1.38 +  by (fact continuous_snd)
    1.39  
    1.40 -lemma isCont_Pair [simp]:
    1.41 -  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    1.42 -  unfolding isCont_def by (rule tendsto_Pair)
    1.43 +lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    1.44 +  by (fact continuous_Pair)
    1.45  
    1.46  subsubsection {* Separation axioms *}
    1.47