3 theorem updates from zero-dim. to str. zero-dim., and a theorem for when str. zero-dim. implies zero-dim.

[Moniker1998]

T300:
Removed reference, added direct proof (complete regularity unnecessary)

T465:
The paper proves strongly zero-dimensional (haven't checked the paper, I trust on the people who introduced T465)

T697:
Updated proof to str. zero-dim. (complete regularity unnecessary)

T768:
completely regular + str. zero-dim. implies zero-dim.
(it's quite obvious we need enough zero-sets here, so complete regularity is obvious assumption;
note that we have inequality $\text{ind}(X)\leq \text{Ind}(X)$ for $T_1$ and for regular spaces in Charalambous, this doesn't lead to any new theorems since ultranormal spaces which are either $T_1$ or regular are always completely regular and str. zero-dim)
(assumption of functionally Hausdorff instead of completely regular leads to totally separated spaces, this will be in different PR)

@prabau

[prabau]

T465: I think we should change it to [ GO-space + totally disconnected => ultranormal ]
The new version is what the paper proves actually, i.e., that $Ind(X)=0$ in this case. (The proof is just as easy; it does not use zero-sets in any way.)

As far implications go, it's equivalent to having strongly zero-dim as conclusion. But the pi-base deductions will be simpler.

(As an aside, I find that paper of Brunet poorly written. Not sure if it's typical French fashion, but he completely disregarded works of other authors in that area, and came up with his own terminology to develop what he wanted. He got the result, but it could have been done better.)

Should we mention in the P218 README that ultranormal corresponds to "Ind(X) = 0" after all? Maybe it would be useful for a situation like this one even if we don't formally define the large inductive dimension (yet).

Alternatively, we should mention in T465 that in Theorem 5.1 of the paper, ultranormal corresponds to "Ind(X) = 0".

[prabau]

T697: It's fine, except that it should say "disjoint cozero sets ...".

But just for my information:
The fact that disjoint zero sets are contained in disjoint cozero sets is basic (if $f_i:X\to[0,1]$ has zero set equal to $Z_i$, one can form $h=f_1/(f_1+f_2)$ with $h^{-1}(0)=Z_1$ and $h^{-1}(1)=Z_2$, etc, easy stuff).
Do you know of a reference that mentions this basic fact?

[prabau]

Maybe you could add the removal of the bullet point in the README to this PR, since it will be merged first.

[Moniker1998]

Maybe you could add the removal of the bullet point in the README to this PR, since it will be merged first.

it'll be merged anyway so I see no point

[Moniker1998]

Should we mention in the P218 README that ultranormal corresponds to "Ind(X) = 0" after all? Maybe it would be useful for a situation like this one even if we don't formally define the large inductive dimension (yet).

I could mention that ultranormal is equivalent to $\text{dim}(X)\leq 0, \text{Ind}(X)\leq 0$ and $\text{Ind}_0(X)\leq 0$ of Charalambous

[Moniker1998]

T697: It's fine, except that it should say "disjoint cozero sets ...".

But just for my information: The fact that disjoint zero sets are contained in disjoint cozero sets is basic (if f i : X → [ 0 , 1 ] has zero set equal to Z i , one can form h = f 1 / ( f 1 + f 2 ) with h − 1 ( 0 ) = Z 1 and h − 1 ( 1 ) = Z 2 , etc, easy stuff). Do you know of a reference that mentions this basic fact?

Off the top of my head, Engelking is one. But maybe Gillman and Jerison too

[Moniker1998]

@prabau I've updated P217 and P218 with mention of what these properties are equivalent to for dimension functions in Charalambous. Hopefully that's enough

[yhx-12243]

One other thing: T464 is now redundant by following:

If you agree to remove T464, you can change T768 in the place of T464.