add paracompact properties and arens space props

[StevenClontz]

No description provided.

[prabau]

Nice addition for the paracompact related properties. You kind of beat me to it for the Arens space, as I was in the middle of adding various properties as well. Maybe I can just comment on what you have and then add more afterwards.

[prabau]

The definition of ultraparacompact in J. Van Name's paper includes Hausdorff. As we discussed before, it allows more generality if we don't include that in the pi-base definition. But we should make a note of this.

Do you know where the term "ultraparacompact" originated? A google search gives some papers using it from the 1990's and 1980's and even earlier maybe.

[StevenClontz]

I don't know much about ultraparacompact; I was able to see quickly that the Arens space must have this property (whatever it was named), then found the preprint that showed the elegant sufficient conditions of Lindelof + 0-dim.

[prabau]

I made a few changes. Please take a look.

For T343 in particular, Engelking mentions on p. 317 that a star-finite family of sets is not necessarily locally finite, but it will be the case if all the sets are open. So I added that the sets were open.

[prabau]

Also fixed typo (properites --> properties) in the title of https://math.stackexchange.com/questions/4673615 that we are referring to. But that should be fixed in mathse as well so things match up.

[StevenClontz]

Looks fine to me. I'll merge after getting an approving review. I requested Chris but it's okay if Patrick make the approval instead since 11f4cd7 and 313cabd are pretty light amendments.

[prabau]

I want to add something, but can you remind me how to search for an MR article reference number without logging in to it?

Want to get the MR ref for https://eudml.org/doc/161976.

[StevenClontz]

I don't think you can look things up without having access - you can only follow certain links (like the ones we generate on pi-base) once an MR number is known.

MR0261565

It's also Zbl 0182.25501 which you can use without having a subscription. As noted in #95 we should support these, but don't today.

[prabau]

Some older papers seem to use a slightly different definition for ultraparacompact in terms of a locally finite refinement instead of a partitioning refinement. The two notions are equivalent, as show in Ellis (Math. Ann. 1970), which seems to be the first to use the terminology "ultraparacompact", at least in English. (The article mentions Ponomarev looked at these spaces in 1962 in Russian.) So I added mention of both defs.

If you are ok with that, I'll approve.

[StevenClontz]

Sounds good to me.