P85: Basically disconnected

[prabau]

Add property P85: Basically disconnected.
(Note: this is without any specific separation axiom).

A few simple theorems to start with.

[prabau]

@Moniker1998 Would you be interested in reviewing this?

I took the opportunity to add to Extremally disconnected some of the meta-properties we discussed before.

[prabau]

For the definition of cozero set, there are many ways to express it. In an earlier version, I had the set of points where $f(x)>0$ for a continuous function $f:X\to[0,1]$. Later changed the codomain to $\mathbb R$. None of this matters, but what's your opinion on $[0,1]$?

[Moniker1998]

I think its more classical to write those properties in terms of functions into $\mathbb{R}$, and its just, more pleasant to my eyes I suppose. But it doesn't matter as you say.

[Moniker1998]

One theorem I'd like you to add is that basically disconnected Tychonoff spaces are cozero complemented.

[prabau]

Updated T673 [P-space + T3.5 => cozero complemented]
to [Basically disconnected + T3.5 => cozero complemented].