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