diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Limits.thy	Sun May 07 14:52:53 2023 +0100
@@ -3251,4 +3251,21 @@
   for f :: "real \<Rightarrow> real"
   using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp: neq_iff)
 
+lemma Lim_topological:
+  "(f \<longlongrightarrow> l) net \<longleftrightarrow>
+    trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+  unfolding tendsto_def trivial_limit_eq by auto
+
+lemma eventually_within_Un:
+  "eventually P (at x within (s \<union> t)) \<longleftrightarrow>
+    eventually P (at x within s) \<and> eventually P (at x within t)"
+  unfolding eventually_at_filter
+  by (auto elim!: eventually_rev_mp)
+
+lemma Lim_within_Un:
+ "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
+  (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
+  unfolding tendsto_def
+  by (auto simp: eventually_within_Un)
+
 end