--- a/src/HOL/Topological_Spaces.thy Thu Oct 07 10:34:48 2021 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Oct 06 14:19:46 2021 +0200
@@ -788,6 +788,11 @@
lemma tendsto_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> ((\<lambda>x. f x) \<longlongrightarrow> l) net"
by (rule topological_tendstoI) (auto elim: eventually_mono)
+(* Contributed by Dominique Unruh *)
+lemma tendsto_principal_singleton[simp]:
+ shows "(f \<longlongrightarrow> f x) (principal {x})"
+ unfolding tendsto_def eventually_principal by simp
+
end
lemma (in topological_space) filterlim_within_subset:
@@ -3438,7 +3443,6 @@
end
-
subsubsection \<open>Uniformly continuous functions\<close>
definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool"