--- a/src/HOL/Topological_Spaces.thy Sat Jun 02 22:57:44 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Sun Jun 03 15:22:30 2018 +0100
@@ -1353,6 +1353,12 @@
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+lemma LIMSEQ_lessThan_iff_atMost:
+ shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
+ apply (subst LIMSEQ_Suc_iff [symmetric])
+ apply (simp only: lessThan_Suc_atMost)
+ done
+
lemma LIMSEQ_unique: "X \<longlonglongrightarrow> a \<Longrightarrow> X \<longlonglongrightarrow> b \<Longrightarrow> a = b"
for a b :: "'a::t2_space"
using trivial_limit_sequentially by (rule tendsto_unique)