# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1697040153 -3600
# Node ID f229090cb8a3be70b0801dbac61d231d93306496
# Parent  23215f71ab69b84ee374137b6cf49cb674f3b0b3
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits

diff -r 23215f71ab69 -r f229090cb8a3 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Wed Oct 11 14:25:14 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Wed Oct 11 17:02:33 2023 +0100
@@ -9,9 +9,14 @@
   where "nhdsin X a =
            (if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"
 
-definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
-  where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
+definition atin_within :: "['a topology, 'a, 'a set] \<Rightarrow> 'a filter"
+  where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \<inter> S - {a}))"
 
+abbreviation atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
+  where "atin X a \<equiv> atin_within X a UNIV"
+
+lemma atin_def: "atin X a = inf (nhdsin X a) (principal (topspace X - {a}))"
+  by (simp add: atin_within_def)
 
 lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
   and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
@@ -28,18 +33,23 @@
   finally show ?thesis using True by simp
 qed auto
 
+lemma eventually_atin_within:
+  "eventually P (atin_within X a S) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+proof (cases "a \<in> topspace X")
+  case True
+  hence "eventually P (atin_within X a S) \<longleftrightarrow> 
+         (\<exists>T. openin X T \<and> a \<in> T \<and>
+          (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+    by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
+  also have "\<dots> \<longleftrightarrow> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+    using openin_subset by (intro ex_cong) auto
+  finally show ?thesis by (simp add: True)
+qed (simp add: atin_within_def)
+
 lemma eventually_atin:
   "eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
              (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
-proof (cases "a \<in> topspace X")
-  case True
-  hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
-           a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
-    by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
-  also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
-    using openin_subset by (intro ex_cong) auto
-  finally show ?thesis by (simp add: True)
-qed auto
+  by (auto simp add: eventually_atin_within)
 
 lemma nontrivial_limit_atin:
    "atin X a \<noteq> bot \<longleftrightarrow> a \<in> X derived_set_of topspace X"
@@ -64,12 +74,50 @@
   qed
 qed
 
+lemma eventually_atin_subtopology:
+  assumes "a \<in> topspace X"
+  shows "eventually P (atin (subtopology X S) a) \<longleftrightarrow> 
+    (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
+  using assms by (simp add: eventually_atin)
+
+lemma eventually_within_imp:
+   "eventually P (atin_within X a S) \<longleftrightarrow> eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) (atin X a)"
+  by (auto simp add: eventually_atin_within eventually_atin)
+
+lemma atin_subtopology_within:
+  assumes "a \<in> S"
+  shows "atin (subtopology X S) a = atin_within X a S"
+proof -
+  have "eventually P (atin (subtopology X S) a) \<longleftrightarrow> eventually P (atin_within X a S)" for P
+    unfolding eventually_atin eventually_atin_within openin_subtopology
+    using assms by auto
+  then show ?thesis
+    by (meson le_filter_def order.eq_iff)
+qed
+
+lemma atin_subtopology_within_if:
+  shows "atin (subtopology X S) a = (if a \<in> S then atin_within X a S else bot)"
+  by (simp add: atin_subtopology_within)
+
+lemma trivial_limit_atpointof_within:
+   "trivial_limit(atin_within X a S) \<longleftrightarrow>
+        (a \<notin> X derived_set_of S)"
+  by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)
+
+lemma derived_set_of_trivial_limit:
+   "a \<in> X derived_set_of S \<longleftrightarrow> \<not> trivial_limit(atin_within X a S)"
+  by (simp add: trivial_limit_atpointof_within)
+
 
 subsection\<open>Limits in a topological space\<close>
 
 definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
   "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
 
+lemma limit_within_subset:
+   "\<lbrakk>limitin X f l (atin_within Y a S); T \<subseteq> S\<rbrakk> \<Longrightarrow> limitin X f l (atin_within Y a T)"
+  by (smt (verit) eventually_atin_within limitin_def subset_eq)
+
 lemma limitinD: "\<lbrakk>limitin X f l F; openin X U; l \<in> U\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. f x \<in> U) F"
   by (simp add: limitin_def)
 
@@ -217,10 +265,7 @@
   assume R: ?rhs
   then show ?lhs
     apply (auto simp: continuous_map_def topcontinuous_at_def)
-    apply (subst openin_subopen, safe)
-    apply (drule bspec, assumption)
-    using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
-    done
+    by (smt (verit, del_insts) mem_Collect_eq openin_subopen openin_subset subset_eq)
 qed
 
 lemma continuous_map_atin:
@@ -231,6 +276,11 @@
    "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limitin Y f b (atin X a)"
   by (auto simp: continuous_map_atin)
 
+lemma limit_continuous_map_within:
+   "\<lbrakk>continuous_map (subtopology X S) Y f; a \<in> S; a \<in> topspace X\<rbrakk>
+    \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
+  by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)
+
 
 subsection\<open>Combining theorems for continuous functions into the reals\<close>
 
diff -r 23215f71ab69 -r f229090cb8a3 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Wed Oct 11 14:25:14 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Wed Oct 11 17:02:33 2023 +0100
@@ -3371,74 +3371,6 @@
     using empty_completely_metrizable_space by auto
 qed 
 
-
-subsection \<open>The "atin-within" filter for topologies\<close>
-
-(*FIXME: replace original definition of atin to be an abbreviation, like at / at_within
-    ("atin (_) (_)/ within (_)" [1000, 60] 60)*)
-definition atin_within :: "['a topology, 'a, 'a set] \<Rightarrow> 'a filter"
-  where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \<inter> S - {a}))"
-
-lemma atin_within_UNIV [simp]:
-  shows "atin_within X a UNIV = atin X a"
-  by (simp add: atin_def atin_within_def)
-
-lemma eventually_atin_subtopology:
-  assumes "a \<in> topspace X"
-  shows "eventually P (atin (subtopology X S) a) \<longleftrightarrow> 
-    (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
-  using assms by (simp add: eventually_atin)
-
-lemma eventually_atin_within:
-  "eventually P (atin_within X a S) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
-proof (cases "a \<in> topspace X")
-  case True
-  hence "eventually P (atin_within X a S) \<longleftrightarrow> 
-         (\<exists>T. openin X T \<and> a \<in> T \<and>
-          (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
-    by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
-  also have "\<dots> \<longleftrightarrow> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
-    using openin_subset by (intro ex_cong) auto
-  finally show ?thesis by (simp add: True)
-qed (simp add: atin_within_def)
-
-lemma eventually_within_imp:
-   "eventually P (atin_within X a S) \<longleftrightarrow> eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) (atin X a)"
-  by (auto simp add: eventually_atin_within eventually_atin)
-
-lemma limit_within_subset:
-   "\<lbrakk>limitin X f l (atin_within Y a S); T \<subseteq> S\<rbrakk> \<Longrightarrow> limitin X f l (atin_within Y a T)"
-  by (smt (verit) eventually_atin_within limitin_def subset_eq)
-
-lemma atin_subtopology_within:
-  assumes "a \<in> S"
-  shows "atin (subtopology X S) a = atin_within X a S"
-proof -
-  have "eventually P (atin (subtopology X S) a) \<longleftrightarrow> eventually P (atin_within X a S)" for P
-    unfolding eventually_atin eventually_atin_within openin_subtopology
-    using assms by auto
-  then show ?thesis
-    by (meson le_filter_def order.eq_iff)
-qed
-
-lemma limit_continuous_map_within:
-   "\<lbrakk>continuous_map (subtopology X S) Y f; a \<in> S; a \<in> topspace X\<rbrakk>
-    \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
-  by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)
-
-lemma atin_subtopology_within_if:
-  shows "atin (subtopology X S) a = (if a \<in> S then atin_within X a S else bot)"
-  by (simp add: atin_subtopology_within)
-
-lemma trivial_limit_atpointof_within:
-   "trivial_limit(atin_within X a S) \<longleftrightarrow>
-        (a \<notin> X derived_set_of S)"
-  by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)
-
-lemma derived_set_of_trivial_limit:
-   "a \<in> X derived_set_of S \<longleftrightarrow> \<not> trivial_limit(atin_within X a S)"
-  by (simp add: trivial_limit_atpointof_within)
-
     
 subsection\<open>More sequential characterizations in a metric space\<close>
 
diff -r 23215f71ab69 -r f229090cb8a3 src/HOL/Analysis/Urysohn.thy
--- a/src/HOL/Analysis/Urysohn.thy	Wed Oct 11 14:25:14 2023 +0100
+++ b/src/HOL/Analysis/Urysohn.thy	Wed Oct 11 17:02:33 2023 +0100
@@ -4562,8 +4562,7 @@
         with that \<open>a \<in> topspace X\<close> 
         obtain U where U: "openin X U" "a \<in> U" "l \<in> M"
           and Uless: "\<forall>x\<in>U - {a}. x \<in> S \<longrightarrow> f x \<in> M \<and> d (f x) l < \<epsilon>/2"
-          unfolding limitin_metric eventually_within_imp eventually_atin
-          using half_gt_zero by blast
+          unfolding limitin_metric eventually_atin_within by (metis Diff_iff insertI1  half_gt_zero [OF \<open>\<epsilon>>0\<close>])
         show "\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
         proof (intro exI strip conjI)
           fix x y
@@ -4653,7 +4652,7 @@
           qed
           ultimately show "\<forall>\<^sub>F x in atin_within X a S. f x \<in> M \<and> d (f x) b < \<epsilon>"
             using fim U
-            apply (simp add: eventually_atin eventually_within_imp del: divide_const_simps flip: image_subset_iff_funcset)
+            apply (simp add: eventually_atin_within del: divide_const_simps flip: image_subset_iff_funcset)
             by (smt (verit, del_insts) Diff_iff Int_iff imageI insertI1 openin_subset subsetD)
         qed
         then show ?thesis ..