Almost discrete - door cleanup

[prabau]

Many spaces are Door because they are Almost discrete. But they were often asserting Door and then deriving Almost discrete in complicated ways. Change that to assert Almost discrete and derive Door immediately.

Also added the previously unknown Door = false for S34 (ordinal space $\omega+\omega+1$).

[yhx-12243]

Also we can add hereditarily to the meta-properties of door, then easily deduce S36 ($\omega_1 + 1$), S141 ($\omega_1 + 1 + \omega^*$), S181 ($\sigma \left( \omega_1 + 1 \right)^\omega$) is not Door.

Thus door can got thoroughly cleaned with the help of remaining theorems in #821.

[prabau]

@yhx-12243 thanks for the comment. We should add that meta-property to Door. I'll merge this PR for the moment.

As discussed before, if you want to take up writing new PRs for some of results remaining from #821, that would be great. But please do NOT blindly copy what was there before. It should be reasoned and written as if it were a brand new PR, and please only one or two results at a time in a new PR.

If you intend to do that, the work should be coordinated with @danflapjax probably, in case he has some idea of the best way to approach that.

[yhx-12243]

@yhx-12243 thanks for the comment. We should add that meta-property to Door. I'll merge this PR for the moment.

Yes after adding meta-property to Door, we can (manually) add the trait S36, S141, S181 that none of them are Door. Then once #821 gets merged, the Door trait gets a completely cleanup.

As discussed before, if you want to take up writing new PRs for some of results remaining from #821, that would be great. But please do NOT blindly copy what was there before. It should be reasoned and written as if it were a brand new PR, and please only one or two results at a time in a new PR.

If you intend to do that, the work should be coordinated with @danflapjax probably, in case he has some idea of the best way to approach that.

Basically I'll not work on #821 anymore and let it alone to @danflapjax.

[prabau]

Ok. I'll try to summarize in #821 what remains to be done.