Skip to content

Commit

Permalink
fixing build
Browse files Browse the repository at this point in the history
  • Loading branch information
zstone1 committed May 3, 2023
1 parent 32f9f61 commit 60b9d7e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/cantor.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
End alexandroff_hausdorff.

0 comments on commit 60b9d7e

Please sign in to comment.