--- a/src/HOL/Topological_Spaces.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Aug 12 10:09:29 2023 +0100
@@ -1220,6 +1220,11 @@
"f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
unfolding tendsto_def eventually_sequentially by auto
+lemma closed_sequentially:
+ assumes "closed S" and "\<And>n. f n \<in> S" and "f \<longlonglongrightarrow> l"
+ shows "l \<in> S"
+ by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)
+
subsection \<open>Monotone sequences and subsequences\<close>