--- a/src/HOL/Analysis/T1_Spaces.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy Mon Apr 01 17:02:43 2019 +0100
@@ -411,7 +411,7 @@
"\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> closedin X S \<longleftrightarrow> S \<subseteq> topspace X"
by (meson closedin_Hausdorff_finite closedin_def)
-lemma derived_set_of_infinite_open_in:
+lemma derived_set_of_infinite_openin:
"Hausdorff_space X
\<Longrightarrow> X derived_set_of S =
{x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"