Dieudonne complete + monotonically normal implies paracompact

[Moniker1998]

Follows from theorem of Balogh and Rudin as in the link. I have read the proof of theorem II before, so all I had to do is brush up on what screenable means and equivalence with paracompactness + the article of Engelking and Lutzer. So I can vouch for correctness of theorem I.

[prabau]

This is a very deep result. To help the understanding of all this, how about putting this PR on hold and start by adding the screenable property to pi-base?

[Moniker1998]

@prabau we could. Sorry for my previous comment. I meant strongly screenable is equivalent to paracompactness with good enough separation properties, screenable is not. We could add it but I don't see a particular reason to. Why do you want to add it? And why do you want to put this PR on hold?

Theorem I uses screenable in its proof that's true (with it essentially being the definition of screenable if not for the stationary subset of uncountable regular cardinal condition), but the proof, located in Nagata, that normal + countably paracompact + screenable implies strongly screenable and so paracompact, is easy.

Strongly screenable implies paracompact is part of equivalences of paracompactness in Engelking.

[Moniker1998]

How about we finish with this PR (which does not require screenable to be in pi-base, or helps in any deductions, as far as I'm aware), raise an issue to add screenable and strongly screenable properties to pi-base, and then later, add them?