Deleted sequence of intervals topology

[david20000813]

As suggested in #926.

[Almanzoris]

Nice! I will review it in detail tomorrow.

[Almanzoris]

I find it good. Nice proofs!

[Almanzoris]

In #926, you say that, as far as you can tell, it is a new construction. I wonder if you are allowed to add your name to the space's name, like it was done for S100.

[david20000813]

@Almanzoris The construction is quite close to that of S56, Smirnov's deleted sequence topology, so, unlike S100, I wouldn't be surprised if this has been thought of before and I'm just unaware of it, which is why I chose to not add my name to the space's name.

[prabau]

@david20000813 One thing I forgot to mention.

When you do a "squash and merge", it is recommended to first blank out the associated description before clicking on "squash and merge". I.e., only keep the title.

For an explanation, see
#912 (comment) and the following comment,
and #779 (comment).

[david20000813]

@prabau Understood. Thanks for letting me know.