2741 apply (auto dest!: bspec) |
2741 apply (auto dest!: bspec) |
2742 apply (rule_tac x="e/2" in exI, force+) |
2742 apply (rule_tac x="e/2" in exI, force+) |
2743 done |
2743 done |
2744 |
2744 |
2745 lemma Times_in_interior_subtopology: |
2745 lemma Times_in_interior_subtopology: |
2746 fixes U :: "('a::metric_space \<times> 'b::metric_space) set" |
|
2747 assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U" |
2746 assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U" |
2748 obtains V W where "openin (subtopology euclidean S) V" "x \<in> V" |
2747 obtains V W where "openin (subtopology euclidean S) V" "x \<in> V" |
2749 "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U" |
2748 "openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U" |
2750 proof - |
2749 proof - |
2751 from assms obtain e where "e > 0" and "U \<subseteq> S \<times> T" |
2750 from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T" |
2752 and e: "\<And>x' y'. \<lbrakk>x'\<in>S; y'\<in>T; dist (x', y') (x, y) < e\<rbrakk> \<Longrightarrow> (x', y') \<in> U" |
2751 by (auto simp: openin_open) |
2753 by (force simp: openin_euclidean_subtopology_iff) |
2752 from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>] |
2754 with assms have "x \<in> S" "y \<in> T" |
2753 obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E" |
2755 by auto |
2754 by blast |
2756 show ?thesis |
2755 show ?thesis |
2757 proof |
2756 proof |
2758 show "openin (subtopology euclidean S) (ball x (e/2) \<inter> S)" |
2757 show "openin (subtopology euclidean S) (E1 \<inter> S)" |
2759 by (simp add: Int_commute openin_open_Int) |
2758 "openin (subtopology euclidean T) (E2 \<inter> T)" |
2760 show "x \<in> ball x (e / 2) \<inter> S" |
2759 using \<open>open E1\<close> \<open>open E2\<close> |
2761 by (simp add: \<open>0 < e\<close> \<open>x \<in> S\<close>) |
2760 by (auto simp: openin_open) |
2762 show "openin (subtopology euclidean T) (ball y (e/2) \<inter> T)" |
2761 show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T" |
2763 by (simp add: Int_commute openin_open_Int) |
2762 using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto |
2764 show "y \<in> ball y (e / 2) \<inter> T" |
2763 show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U" |
2765 by (simp add: \<open>0 < e\<close> \<open>y \<in> T\<close>) |
2764 using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close> |
2766 show "(ball x (e / 2) \<inter> S) \<times> (ball y (e / 2) \<inter> T) \<subseteq> U" |
2765 by (auto simp: ) |
2767 by clarify (simp add: e dist_Pair_Pair \<open>0 < e\<close> dist_commute sqrt_sum_squares_half_less) |
|
2768 qed |
2766 qed |
2769 qed |
2767 qed |
2770 |
2768 |
2771 lemma openin_Times_eq: |
2769 lemma openin_Times_eq: |
2772 fixes S :: "'a::metric_space set" and T :: "'b::metric_space set" |
2770 fixes S :: "'a::topological_space set" and T :: "'b::topological_space set" |
2773 shows |
2771 shows |
2774 "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow> |
2772 "openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow> |
2775 S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'" |
2773 S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'" |
2776 (is "?lhs = ?rhs") |
2774 (is "?lhs = ?rhs") |
2777 proof (cases "S' = {} \<or> T' = {}") |
2775 proof (cases "S' = {} \<or> T' = {}") |
2809 "closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow> |
2807 "closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow> |
2810 closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')" |
2808 closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')" |
2811 unfolding closedin_closed using closed_Times by blast |
2809 unfolding closedin_closed using closed_Times by blast |
2812 |
2810 |
2813 lemma Lim_transform_within_openin: |
2811 lemma Lim_transform_within_openin: |
2814 fixes a :: "'a::metric_space" |
|
2815 assumes f: "(f \<longlongrightarrow> l) (at a within T)" |
2812 assumes f: "(f \<longlongrightarrow> l) (at a within T)" |
2816 and "openin (subtopology euclidean T) S" "a \<in> S" |
2813 and "openin (subtopology euclidean T) S" "a \<in> S" |
2817 and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x" |
2814 and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x" |
2818 shows "(g \<longlongrightarrow> l) (at a within T)" |
2815 shows "(g \<longlongrightarrow> l) (at a within T)" |
2819 proof - |
2816 proof - |
2820 obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball a \<epsilon> \<inter> T \<subseteq> S" |
2817 have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a" |
2821 using assms by (force simp: openin_contains_ball) |
2818 by (simp add: eventually_at_filter) |
2822 then have "a \<in> ball a \<epsilon>" |
2819 moreover |
2823 by simp |
2820 from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U" |
2824 show ?thesis |
2821 by (auto simp: openin_open) |
2825 by (rule Lim_transform_within [OF f \<open>0 < \<epsilon>\<close> eq]) (use \<epsilon> in \<open>auto simp: dist_commute subset_iff\<close>) |
2822 then have "a \<in> U" using \<open>a \<in> S\<close> by auto |
|
2823 from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>] |
|
2824 have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto |
|
2825 ultimately |
|
2826 have "\<forall>\<^sub>F x in at a within T. f x = g x" |
|
2827 by eventually_elim (auto simp: \<open>S = _\<close> eq) |
|
2828 then show ?thesis using f |
|
2829 by (rule Lim_transform_eventually) |
2826 qed |
2830 qed |
2827 |
2831 |
2828 lemma closure_Int_ballI: |
2832 lemma closure_Int_ballI: |
2829 fixes S :: "'a :: metric_space set" |
|
2830 assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}" |
2833 assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}" |
2831 shows "S \<subseteq> closure T" |
2834 shows "S \<subseteq> closure T" |
2832 proof (clarsimp simp: closure_approachable dist_commute) |
2835 proof (clarsimp simp: closure_iff_nhds_not_empty) |
2833 fix x and e::real |
2836 fix x and A and V |
2834 assume "x \<in> S" "0 < e" |
2837 assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}" |
2835 with assms [of "S \<inter> ball x e"] show "\<exists>y\<in>T. dist x y < e" |
2838 then have "openin (subtopology euclidean S) (A \<inter> V \<inter> S)" |
2836 by force |
2839 by (auto simp: openin_open intro!: exI[where x="V"]) |
|
2840 moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close> |
|
2841 by auto |
|
2842 ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}" |
|
2843 by (rule assms) |
|
2844 with \<open>T \<inter> A = {}\<close> show False by auto |
2837 qed |
2845 qed |
2838 |
2846 |
2839 lemma continuous_on_open_gen: |
2847 lemma continuous_on_open_gen: |
2840 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
|
2841 assumes "f ` S \<subseteq> T" |
2848 assumes "f ` S \<subseteq> T" |
2842 shows "continuous_on S f \<longleftrightarrow> |
2849 shows "continuous_on S f \<longleftrightarrow> |
2843 (\<forall>U. openin (subtopology euclidean T) U |
2850 (\<forall>U. openin (subtopology euclidean T) U |
2844 \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))" |
2851 \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))" |
2845 (is "?lhs = ?rhs") |
2852 (is "?lhs = ?rhs") |
2846 proof |
2853 proof |
2847 assume ?lhs |
2854 assume ?lhs |
2848 then show ?rhs |
2855 then show ?rhs |
2849 apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff) |
2856 by (clarsimp simp add: continuous_openin_preimage_eq openin_open) |
2850 by (metis assms image_subset_iff) |
2857 (metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1) |
2851 next |
2858 next |
2852 have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e |
|
2853 by (simp add: Int_commute openin_open_Int) |
|
2854 assume R [rule_format]: ?rhs |
2859 assume R [rule_format]: ?rhs |
2855 show ?lhs |
2860 show ?lhs |
2856 proof (clarsimp simp add: continuous_on_iff) |
2861 proof (clarsimp simp add: continuous_openin_preimage_eq) |
2857 fix x and e::real |
2862 fix U::"'a set" |
2858 assume "x \<in> S" and "0 < e" |
2863 assume "open U" |
2859 then have x: "x \<in> S \<inter> (f -` ball (f x) e \<inter> f -` T)" |
2864 then have "openin (subtopology euclidean S) (S \<inter> f -` (U \<inter> T))" |
2860 using assms by auto |
2865 by (metis R inf_commute openin_open) |
2861 show "\<exists>d>0. \<forall>x'\<in>S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
2866 then show "openin (subtopology euclidean S) (S \<inter> f -` U)" |
2862 using R [of "ball (f x) e \<inter> T"] x |
2867 by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int) |
2863 by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute) |
|
2864 qed |
2868 qed |
2865 qed |
2869 qed |
2866 |
2870 |
2867 lemma continuous_openin_preimage: |
2871 lemma continuous_openin_preimage: |
2868 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
2872 "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk> |
2869 shows |
|
2870 "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk> |
|
2871 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)" |
2873 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)" |
2872 by (simp add: continuous_on_open_gen) |
2874 by (simp add: continuous_on_open_gen) |
2873 |
2875 |
2874 lemma continuous_on_closed_gen: |
2876 lemma continuous_on_closed_gen: |
2875 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
|
2876 assumes "f ` S \<subseteq> T" |
2877 assumes "f ` S \<subseteq> T" |
2877 shows "continuous_on S f \<longleftrightarrow> |
2878 shows "continuous_on S f \<longleftrightarrow> |
2878 (\<forall>U. closedin (subtopology euclidean T) U |
2879 (\<forall>U. closedin (subtopology euclidean T) U |
2879 \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))" |
2880 \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))" |
2880 (is "?lhs = ?rhs") |
2881 (is "?lhs = ?rhs") |
2881 proof - |
2882 proof - |
2882 have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U |
2883 have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U |
2883 using assms by blast |
2884 using assms by blast |
2884 show ?thesis |
2885 show ?thesis |
2885 proof |
2886 proof |
2899 by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology) |
2900 by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology) |
2900 qed |
2901 qed |
2901 qed |
2902 qed |
2902 |
2903 |
2903 lemma continuous_closedin_preimage_gen: |
2904 lemma continuous_closedin_preimage_gen: |
2904 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" |
|
2905 assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U" |
2905 assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U" |
2906 shows "closedin (subtopology euclidean S) (S \<inter> f -` U)" |
2906 shows "closedin (subtopology euclidean S) (S \<inter> f -` U)" |
2907 using assms continuous_on_closed_gen by blast |
2907 using assms continuous_on_closed_gen by blast |
2908 |
2908 |
2909 lemma continuous_transform_within_openin: |
2909 lemma continuous_transform_within_openin: |
2910 fixes a :: "'a::metric_space" |
|
2911 assumes "continuous (at a within T) f" |
2910 assumes "continuous (at a within T) f" |
2912 and "openin (subtopology euclidean T) S" "a \<in> S" |
2911 and "openin (subtopology euclidean T) S" "a \<in> S" |
2913 and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
2912 and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
2914 shows "continuous (at a within T) g" |
2913 shows "continuous (at a within T) g" |
2915 using assms by (simp add: Lim_transform_within_openin continuous_within) |
2914 using assms by (simp add: Lim_transform_within_openin continuous_within) |