[Moniker1998]

Those spaces can be expressed by other properties (metrizable and ultranormal) so I won't be introducing any new theorems other than the equivalence.

It's just so that we can have this property here.

Proof of T772 is a bit long but it's completely elementary so I think it's fine for pi-base.

[prabau]

I think there was also a purely topological notion to express the "ultrametric" property, but I don't remember right now. Will have to look for it.

[prabau]

"Non-Archimedean space" (see Encyclopedia of general topology)

[Moniker1998]

@prabau exact chapter please, I think Encyclopedia cites different definitions in different chapters

[prabau]

The index has the pages. In this case, p. 284 (chap. e-13) and p. 328 (chap. f-7).

[prabau]

It's not exactly the same as ultrametrizable, but it's related.
I.e., ultrametrizable => non-Archimedean.
But it was an open question if there were non-Archimedean non-metrizable spaces in ZFC.

[Moniker1998]

@prabau there's some definitions which imply metrizable and some which don't from what I've seen. I need you to be specific about which definition you are talking about. I believe non-Archimedean is an alias as well

[prabau]

See p. 284. One would have to check some of the references for more details. Anyway, all that is background info, something that could be added later.

[Moniker1998]

@prabau I won't add it, but feel free to add it yourself, in a different PR. I can review it after

[Moniker1998]

@prabau are you able to review this

[prabau]

T771: we can replace this with [ ultrametrizable => ultraparacompact ]
and just reference Van Name's Theorem 11.

[Moniker1998]

@prabau the proof of T771 is essentially proof in Van Name's article, just more clear
what he actually proves there is ultrametrizable => ultranormal

[prabau]

I know it is, but the proof in Van Name seems pretty clear to me (except a few minor typos).
The proof is too long for pi-base.

[prabau]

Also, like you said, the bulk of the proof is to show the space is ultranormal.
The final step is the implication (paracompact + ultranormal => ultraparacompact), which is also known to pi-base. It's T767.

So if you really want more explanation, we can say something like:
See Theorem 11 in {{...}}. The last step of the proof makes use of {T767}.

[Moniker1998]

I know it is, but the proof in Van Name seems pretty clear to me (except a few minor typos). The proof is too long for pi-base.

But I don't like how that proof is written down. It's not as tidy and pieced together. And I really dislike $Max$ notation and the typos

Sure it's a bit long but I imagine you'll get a better idea of what is being shown by reading the proof I wrote down. Why do we need to sacrifice clarity for the sake of keeping it to the rules we put out.

[Moniker1998]

I've shortened the proof a bit. Removed overly elaborate parts

[prabau]

It's more readable. I still think we should change the conclusion to ultraparacompact. (The proof of that is just adding one sentence to your proof to mention T767.)

Among other things, an ultraparacompact conclusion will make more obvious the equivalence
( ultrametrizable <=> metrizable + ultraparacompact ).
(Compare the current "converse" tab in https://topology.pi-base.org/theorems/T000772.)

[Moniker1998]

It's more readable. I still think we should change the conclusion to ultraparacompact. (The proof of that is just adding one sentence to your proof to mention T767.)

What kind of sentence are you referring to? It seems to me like changing this would add at least 3 sentences, and then even those three sentences I'm not completely confident it would be "obvious" that such implications hold.

[yhx-12243]

I think the current state is acceptable, like T462 using ultraparacompact rather than strongly zero-dimensional.

Otherwise one should supply ”Metrizable → Paracompact“ and ”Ultranormal + Paracompact => Ultraparacompact“, however it can be deduced by pi-base automatically.

[prabau]

I have changed T771 to illustrate what I meant. As @yhx-12243 mentioned, we can let pi-base do the work. So the extra one sentence uses an "(Explore)" link, like we also do in many other places.

Also added that the sets $A$ and $B$ have to be disjoint.

[Moniker1998]

@prabau that's fine with me

[prabau]

T772: At first glance, it was difficult to figure out how the bullets fit in the page. Here is a easier layout, I think. Let me know what you think.

[Moniker1998]

@prabau would it be better to enumerate those instead

[prabau]

@prabau would it be better to enumerate those instead

I experimented with that and somehow it did not look as good. You can experiment for yourself in the "preview window" (accessible from the Advanced tab).

[Moniker1998]

@prabau I trust your aesthetic choice, I just didn't know if you tried that already
Also I'm aware of the sandbox, you mentioned it once or twice before already.

[prabau]

I added a reference for T771, as suggested in #1424 (comment)

Ready to go as far as I am concerned.
@Moniker1998 Any further comment?

[Moniker1998]

@prabau I've got nothing