# HG changeset patch
# User immler
# Date 1546883441 -3600
# Node ID 00347595559372a7f5dfd8998b234c0b9f608f83
# Parent  9c22ff18125bc063fbe016da9bf542e746d5fddf
moved generalized lemmas

diff -r 9c22ff18125b -r 003475955593 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Jan 07 18:42:49 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jan 07 18:50:41 2019 +0100
@@ -3556,4 +3556,166 @@
 lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
   by (simp add: closed_vimage continuous_on_eq_continuous_within)
 
+lemma Times_in_interior_subtopology:
+  assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
+  obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
+                    "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
+proof -
+  from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T"
+    by (auto simp: openin_open)
+  from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>]
+  obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E"
+    by blast
+  show ?thesis
+  proof
+    show "openin (subtopology euclidean S) (E1 \<inter> S)"
+      "openin (subtopology euclidean T) (E2 \<inter> T)"
+      using \<open>open E1\<close> \<open>open E2\<close>
+      by (auto simp: openin_open)
+    show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T"
+      using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
+    show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
+      using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
+      by (auto simp: )
+  qed
+qed
+
+lemma closedin_Times:
+  "closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow>
+    closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+  unfolding closedin_closed using closed_Times by blast
+
+lemma openin_Times:
+  "openin (subtopology euclidean S) S' \<Longrightarrow> openin (subtopology euclidean T) T' \<Longrightarrow>
+    openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
+  unfolding openin_open using open_Times by blast
+
+lemma openin_Times_eq:
+  fixes S :: "'a::topological_space set" and T :: "'b::topological_space set"
+  shows
+    "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
+      S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'"
+    (is "?lhs = ?rhs")
+proof (cases "S' = {} \<or> T' = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  then obtain x y where "x \<in> S'" "y \<in> T'"
+    by blast
+  show ?thesis
+  proof
+    assume ?lhs
+    have "openin (subtopology euclidean S) S'"
+      apply (subst openin_subopen, clarify)
+      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
+      using \<open>y \<in> T'\<close>
+       apply auto
+      done
+    moreover have "openin (subtopology euclidean T) T'"
+      apply (subst openin_subopen, clarify)
+      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
+      using \<open>x \<in> S'\<close>
+       apply auto
+      done
+    ultimately show ?rhs
+      by simp
+  next
+    assume ?rhs
+    with False show ?lhs
+      by (simp add: openin_Times)
+  qed
+qed
+
+lemma Lim_transform_within_openin:
+  assumes f: "(f \<longlongrightarrow> l) (at a within T)"
+    and "openin (subtopology euclidean T) S" "a \<in> S"
+    and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "(g \<longlongrightarrow> l) (at a within T)"
+proof -
+  have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a"
+    by (simp add: eventually_at_filter)
+  moreover
+  from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U"
+    by (auto simp: openin_open)
+  then have "a \<in> U" using \<open>a \<in> S\<close> by auto
+  from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>]
+  have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto
+  ultimately
+  have "\<forall>\<^sub>F x in at a within T. f x = g x"
+    by eventually_elim (auto simp: \<open>S = _\<close> eq)
+  then show ?thesis using f
+    by (rule Lim_transform_eventually)
+qed
+
+lemma continuous_on_open_gen:
+  assumes "f ` S \<subseteq> T"
+    shows "continuous_on S f \<longleftrightarrow>
+             (\<forall>U. openin (subtopology euclidean T) U
+                  \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
+     (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
+      (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
+next
+  assume R [rule_format]: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: continuous_openin_preimage_eq)
+    fix U::"'a set"
+    assume "open U"
+    then have "openin (subtopology euclidean S) (S \<inter> f -` (U \<inter> T))"
+      by (metis R inf_commute openin_open)
+    then show "openin (subtopology euclidean S) (S \<inter> f -` U)"
+      by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
+  qed
+qed
+
+lemma continuous_openin_preimage:
+  "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
+        \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
+  by (simp add: continuous_on_open_gen)
+
+lemma continuous_on_closed_gen:
+  assumes "f ` S \<subseteq> T"
+  shows "continuous_on S f \<longleftrightarrow>
+             (\<forall>U. closedin (subtopology euclidean T) U
+                  \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
+    (is "?lhs = ?rhs")
+proof -
+  have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
+    using assms by blast
+  show ?thesis
+  proof
+    assume L: ?lhs
+    show ?rhs
+    proof clarify
+      fix U
+      assume "closedin (subtopology euclidean T) U"
+      then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
+        using L unfolding continuous_on_open_gen [OF assms]
+        by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
+    qed
+  next
+    assume R [rule_format]: ?rhs
+    show ?lhs
+      unfolding continuous_on_open_gen [OF assms]
+      by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
+  qed
+qed
+
+lemma continuous_closedin_preimage_gen:
+  assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
+    shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
+using assms continuous_on_closed_gen by blast
+
+lemma continuous_transform_within_openin:
+  assumes "continuous (at a within T) f"
+    and "openin (subtopology euclidean T) S" "a \<in> S"
+    and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "continuous (at a within T) g"
+  using assms by (simp add: Lim_transform_within_openin continuous_within)
+
+
 end
diff -r 9c22ff18125b -r 003475955593 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Mon Jan 07 18:42:49 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Mon Jan 07 18:50:41 2019 +0100
@@ -132,11 +132,6 @@
     openin (subtopology euclidean T) S"
   by (auto simp: openin_open)
 
-lemma openin_Times:
-  "openin (subtopology euclidean S) S' \<Longrightarrow> openin (subtopology euclidean T) T' \<Longrightarrow>
-    openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
-  unfolding openin_open using open_Times by blast
-
 lemma closedin_compact:
    "\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
 by (metis closedin_closed compact_Int_closed)
@@ -179,6 +174,22 @@
   shows "\<lbrakk>openin (subtopology euclidean U) S; x \<in> S; x islimpt U\<rbrakk> \<Longrightarrow> infinite S"
   by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)
 
+lemma closure_Int_ballI:
+  assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
+  shows "S \<subseteq> closure T"
+proof (clarsimp simp: closure_iff_nhds_not_empty)
+  fix x and A and V
+  assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
+  then have "openin (subtopology euclidean S) (A \<inter> V \<inter> S)"
+    by (auto simp: openin_open intro!: exI[where x="V"])
+  moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
+    by auto
+  ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
+    by (rule assms)
+  with \<open>T \<inter> A = {}\<close> show False by auto
+qed
+
+
 subsection \<open>Frontier\<close>
 
 lemma connected_Int_frontier:
diff -r 9c22ff18125b -r 003475955593 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 18:42:49 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jan 07 18:50:41 2019 +0100
@@ -2736,183 +2736,12 @@
    "openin (subtopology euclidean t) s \<longleftrightarrow>
         s \<subseteq> t \<and>
         (\<forall>x \<in> s. \<exists>e. 0 < e \<and> cball x e \<inter> t \<subseteq> s)"
-apply (simp add: openin_contains_ball)
-apply (rule iffI)
-apply (auto dest!: bspec)
-apply (rule_tac x="e/2" in exI, force+)
+  apply (simp add: openin_contains_ball)
+  apply (rule iffI)
+   apply (auto dest!: bspec)
+   apply (rule_tac x="e/2" in exI, force+)
   done
 
-lemma Times_in_interior_subtopology:
-  assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
-  obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
-                    "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
-proof -
-  from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T"
-    by (auto simp: openin_open)
-  from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>]
-  obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E"
-    by blast
-  show ?thesis
-  proof
-    show "openin (subtopology euclidean S) (E1 \<inter> S)"
-      "openin (subtopology euclidean T) (E2 \<inter> T)"
-      using \<open>open E1\<close> \<open>open E2\<close>
-      by (auto simp: openin_open)
-    show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T"
-      using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
-    show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
-      using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
-      by (auto simp: )
-  qed
-qed
-
-lemma openin_Times_eq:
-  fixes S :: "'a::topological_space set" and T :: "'b::topological_space set"
-  shows
-    "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
-      S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'"
-    (is "?lhs = ?rhs")
-proof (cases "S' = {} \<or> T' = {}")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  then obtain x y where "x \<in> S'" "y \<in> T'"
-    by blast
-  show ?thesis
-  proof
-    assume ?lhs
-    have "openin (subtopology euclidean S) S'"
-      apply (subst openin_subopen, clarify)
-      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
-      using \<open>y \<in> T'\<close>
-       apply auto
-      done
-    moreover have "openin (subtopology euclidean T) T'"
-      apply (subst openin_subopen, clarify)
-      apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
-      using \<open>x \<in> S'\<close>
-       apply auto
-      done
-    ultimately show ?rhs
-      by simp
-  next
-    assume ?rhs
-    with False show ?lhs
-      by (simp add: openin_Times)
-  qed
-qed
-
-lemma closedin_Times:
-  "closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow>
-    closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
-  unfolding closedin_closed using closed_Times by blast
-
-lemma Lim_transform_within_openin:
-  assumes f: "(f \<longlongrightarrow> l) (at a within T)"
-    and "openin (subtopology euclidean T) S" "a \<in> S"
-    and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
-  shows "(g \<longlongrightarrow> l) (at a within T)"
-proof -
-  have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a"
-    by (simp add: eventually_at_filter)
-  moreover
-  from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U"
-    by (auto simp: openin_open)
-  then have "a \<in> U" using \<open>a \<in> S\<close> by auto
-  from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>]
-  have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto
-  ultimately
-  have "\<forall>\<^sub>F x in at a within T. f x = g x"
-    by eventually_elim (auto simp: \<open>S = _\<close> eq)
-  then show ?thesis using f
-    by (rule Lim_transform_eventually)
-qed
-
-lemma closure_Int_ballI:
-  assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
-  shows "S \<subseteq> closure T"
-proof (clarsimp simp: closure_iff_nhds_not_empty)
-  fix x and A and V
-  assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
-  then have "openin (subtopology euclidean S) (A \<inter> V \<inter> S)"
-    by (auto simp: openin_open intro!: exI[where x="V"])
-  moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
-    by auto
-  ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
-    by (rule assms)
-  with \<open>T \<inter> A = {}\<close> show False by auto
-qed
-
-lemma continuous_on_open_gen:
-  assumes "f ` S \<subseteq> T"
-    shows "continuous_on S f \<longleftrightarrow>
-             (\<forall>U. openin (subtopology euclidean T) U
-                  \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
-     (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
-      (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
-next
-  assume R [rule_format]: ?rhs
-  show ?lhs
-  proof (clarsimp simp add: continuous_openin_preimage_eq)
-    fix U::"'a set"
-    assume "open U"
-    then have "openin (subtopology euclidean S) (S \<inter> f -` (U \<inter> T))"
-      by (metis R inf_commute openin_open)
-    then show "openin (subtopology euclidean S) (S \<inter> f -` U)"
-      by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
-  qed
-qed
-
-lemma continuous_openin_preimage:
-  "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
-        \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
-  by (simp add: continuous_on_open_gen)
-
-lemma continuous_on_closed_gen:
-  assumes "f ` S \<subseteq> T"
-  shows "continuous_on S f \<longleftrightarrow>
-             (\<forall>U. closedin (subtopology euclidean T) U
-                  \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
-    (is "?lhs = ?rhs")
-proof -
-  have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
-    using assms by blast
-  show ?thesis
-  proof
-    assume L: ?lhs
-    show ?rhs
-    proof clarify
-      fix U
-      assume "closedin (subtopology euclidean T) U"
-      then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
-        using L unfolding continuous_on_open_gen [OF assms]
-        by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
-    qed
-  next
-    assume R [rule_format]: ?rhs
-    show ?lhs
-      unfolding continuous_on_open_gen [OF assms]
-      by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
-  qed
-qed
-
-lemma continuous_closedin_preimage_gen:
-  assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
-    shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
-using assms continuous_on_closed_gen by blast
-
-lemma continuous_transform_within_openin:
-  assumes "continuous (at a within T) f"
-    and "openin (subtopology euclidean T) S" "a \<in> S"
-    and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
-  shows "continuous (at a within T) g"
-  using assms by (simp add: Lim_transform_within_openin continuous_within)
-
 
 subsection \<open>Closed Nest\<close>