diff --git a/theories/cantor.v b/theories/cantor.v index 62e8bcb6e1..35c2ea1d14 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -695,4 +695,4 @@ have : set_surj [set: cantor_space] [set: T] (cst point). by move=> q _; exists point => //; have /negP := xpt q; rewrite negbK => /eqP. by case/Psurj => f cstf; exists f; rewrite -cstf; apply: cst_continuous. Qed. -Section alexandroff_hausdorff. \ No newline at end of file +End alexandroff_hausdorff. \ No newline at end of file