pi-base
Novak space is extremally disconnected
The proof that the extremally disconnected property is preserved by dense sets is really not hard. But we can change the Engelking reference to something more explicit for the benefit of pi-base users. Let me make a suggestion below.
see #1202. We may instead remove all references to that fact here and add a meta-property on the page for the extremally disconnected property. So we would have a common reference available for all spaces that need it.
As for the Novak space itself, I have not taken time to read the description yet, so I cannot comment on it at this point. If anyone else wants to review this, please feel free.
I would add to the definition of the Novak space a reference to item 1 in Counterexamples... to justify the existence of the family $\{P_A:A\in F\}$.
@pzjp The definition of Novak space needs a whole revamp, but this is for another PR https://github.com/pi-base/data/issues/1218
@prabau could this be reviewed? Note that current definition of Novak space on pi-base and in counter-examples is wrong for some set theory reasons (namely $\mathfrak{c}$ need not be a regular cardinal, we could have $\mathfrak{c} = \aleph_{\omega_1}$), but it's not a problem since the definition of Novak space will have that $\mathbb{N} \subseteq X\subseteq \beta\mathbb{N}$ anyway
@prabau this PR should be a no-brainer to review, it's just meta-property of extremally disconnected spaces
The justification for {S108|P49}, which is used here, refers to item #8 for space #111 in S&S. But that is not what that item is showing. We should replace that by a better justification. For example https://math.stackexchange.com/questions/2814978/%c4%8cech-stone-compactification-of-extremally-disconnected-space
@prabau I could cite the more general proposition 2 in https://math.stackexchange.com/a/5025114/476484 if that sounds good to you