src/HOL/Library/Product_Vector.thy
changeset 34110 4c113c744b86
parent 31590 776d6a4c1327
child 36332 3ddb2bc07784
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Nov 23 15:30:32 2009 -0800
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Nov 29 11:31:39 2009 -0800
     1.3 @@ -102,6 +102,42 @@
     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 +lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
    1.20 +  unfolding image_def subset_eq by force
    1.21 +
    1.22 +lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
    1.23 +proof (rule openI)
    1.24 +  fix x assume "x \<in> fst ` S"
    1.25 +  then obtain y where "(x, y) \<in> S" by auto
    1.26 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
    1.27 +    using `open S` unfolding open_prod_def by auto
    1.28 +  from `A \<times> B \<subseteq> S` `y \<in> B` have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
    1.29 +  with `open A` `x \<in> A` have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
    1.30 +  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
    1.31 +qed
    1.32 +
    1.33 +lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
    1.34 +proof (rule openI)
    1.35 +  fix y assume "y \<in> snd ` S"
    1.36 +  then obtain x where "(x, y) \<in> S" by auto
    1.37 +  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
    1.38 +    using `open S` unfolding open_prod_def by auto
    1.39 +  from `A \<times> B \<subseteq> S` `x \<in> A` have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
    1.40 +  with `open B` `y \<in> B` have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
    1.41 +  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
    1.42 +qed
    1.43  
    1.44  subsection {* Product is a metric space *}
    1.45