src/HOL/Library/Product_Vector.thy

 
 instantiation
   "*" :: (topological_space, topological_space) topological_space
 begin
 
-definition topo_prod_def:
-  "topo = {S. \<forall>x\<in>S. \<exists>A\<in>topo. \<exists>B\<in>topo. x \<in> A \<times> B \<and> A \<times> B \<subseteq> S}"
+definition open_prod_def:
+  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
+    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
 
 instance proof
-  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
-    unfolding topo_prod_def by (auto intro: topo_UNIV)
+  show "open (UNIV :: ('a \<times> 'b) set)"
+    unfolding open_prod_def by auto
 next
   fix S T :: "('a \<times> 'b) set"
-  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
-    unfolding topo_prod_def
+  assume "open S" "open T" thus "open (S \<inter> T)"
+    unfolding open_prod_def
     apply clarify
     apply (drule (1) bspec)+
     apply (clarify, rename_tac Sa Ta Sb Tb)
-    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
-    apply (simp add: topo_Int)
-    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
-    apply (simp add: topo_Int)
+    apply (rule_tac x="Sa \<inter> Ta" in exI)
+    apply (rule_tac x="Sb \<inter> Tb" in exI)
+    apply (simp add: open_Int)
     apply fast
     done
 next
-  fix T :: "('a \<times> 'b) set set"
-  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
-    unfolding topo_prod_def Bex_def by fast
+  fix K :: "('a \<times> 'b) set set"
+  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+    unfolding open_prod_def by fast
 qed
 
 end
 
 subsection {* Product is a metric space *}

     done
 next
   (* FIXME: long proof! *)
   (* Maybe it would be easier to define topological spaces *)
   (* in terms of neighborhoods instead of open sets? *)
-  show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
-    unfolding topo_prod_def topo_dist
-    apply (safe, rename_tac S a b)
+  fix S :: "('a \<times> 'b) set"
+  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    unfolding open_prod_def open_dist
+    apply safe
     apply (drule (1) bspec)
     apply clarify
     apply (drule (1) bspec)+
     apply (clarify, rename_tac r s)
     apply (rule_tac x="min r s" in exI, simp)

     apply (drule spec, erule mp)
     apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
     apply (drule spec, erule mp)
     apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
 
-    apply (rename_tac S a b)
     apply (drule (1) bspec)
     apply clarify
     apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
     apply clarify
-    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
+    apply (rule_tac x="{y. dist y a < r}" in exI)
+    apply (rule_tac x="{y. dist y b < s}" in exI)
+    apply (rule conjI)
     apply clarify
     apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
     apply clarify
     apply (rule le_less_trans [OF dist_triangle])
     apply (erule less_le_trans [OF add_strict_right_mono], simp)
-    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
+    apply (rule conjI)
     apply clarify
     apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
     apply clarify
     apply (rule le_less_trans [OF dist_triangle])
     apply (erule less_le_trans [OF add_strict_right_mono], simp)

 
 lemma tendsto_fst:
   assumes "(f ---> a) net"
   shows "((\<lambda>x. fst (f x)) ---> fst a) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "fst a \<in> S"
-  then have "fst -` S \<in> topo" "a \<in> fst -` S"
-    unfolding topo_prod_def
+  fix S assume "open S" "fst a \<in> S"
+  then have "open (fst -` S)" "a \<in> fst -` S"
+    unfolding open_prod_def
     apply simp_all
     apply clarify
-    apply (erule rev_bexI, simp)
-    apply (rule rev_bexI [OF topo_UNIV])
+    apply (rule exI, erule conjI)
+    apply (rule exI, rule conjI [OF open_UNIV])
     apply auto
     done
   with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
     by (rule topological_tendstoD)
   then show "eventually (\<lambda>x. fst (f x) \<in> S) net"

 
 lemma tendsto_snd:
   assumes "(f ---> a) net"
   shows "((\<lambda>x. snd (f x)) ---> snd a) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "snd a \<in> S"
-  then have "snd -` S \<in> topo" "a \<in> snd -` S"
-    unfolding topo_prod_def
+  fix S assume "open S" "snd a \<in> S"
+  then have "open (snd -` S)" "a \<in> snd -` S"
+    unfolding open_prod_def
     apply simp_all
     apply clarify
-    apply (rule rev_bexI [OF topo_UNIV])
-    apply (erule rev_bexI)
+    apply (rule exI, rule conjI [OF open_UNIV])
+    apply (rule exI, erule conjI)
     apply auto
     done
   with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
     by (rule topological_tendstoD)
   then show "eventually (\<lambda>x. snd (f x) \<in> S) net"

 
 lemma tendsto_Pair:
   assumes "(f ---> a) net" and "(g ---> b) net"
   shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "(a, b) \<in> S"
-  then obtain A B where "A \<in> topo" "B \<in> topo" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
-    unfolding topo_prod_def by auto
+  fix S assume "open S" "(a, b) \<in> S"
+  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
+    unfolding open_prod_def by auto
   have "eventually (\<lambda>x. f x \<in> A) net"
-    using `(f ---> a) net` `A \<in> topo` `a \<in> A`
+    using `(f ---> a) net` `open A` `a \<in> A`
     by (rule topological_tendstoD)
   moreover
   have "eventually (\<lambda>x. g x \<in> B) net"
-    using `(g ---> b) net` `B \<in> topo` `b \<in> B`
+    using `(g ---> b) net` `open B` `b \<in> B`
     by (rule topological_tendstoD)
   ultimately
   show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
     by (rule eventually_elim2)
        (simp add: subsetD [OF `A \<times> B \<subseteq> S`])