--- 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
--- 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:
--- 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>