pi-base
Dieudonne complete
Resolves #477 Essentially, completely uniformizable spaces are those spaces whose Kolmogorov quotient is realcompact.
Perhaps some theorems about realcompact spaces could be replaced by those involving completely uniformizable spaces
Later I (or you of others) may propose a property namely “Extent less than every measurable cardinal”, as a complete helper for this. (I've preparing for the property of “Extent < 𝖈”, as mentioned in https://github.com/pi-base/data/pull/1398#issuecomment-3188127998)
@yhx-12243 we could, but we won't be introducing any spaces of size larger than the first measurable cardinal, as far as I know
P164 has its use, and this is the reason why the extent property is not needed
It seems "Dieudonné complete" is a better primary name for this. (see Engelking 8.5.13 and Encyclopedia of General Topology pp. 205, 254, 262.)
See Engelking for more topological characterizations for this, in particular items (2) and (3).
Are you sure about "topologically complete" as an alias? Which source uses that for Dieudonne complete?
If I recall, that term may have been used for various other things as well, maybe for completely metrizable or Cech-complete. It's rather confusing.
@prabau I don't think another alias is bad, I did the same thing with ultranormal property. There shouldn't be confusion as those are just aliases. Thanks for the references by the way. I am trying to go through Engelking's exercise and will add it once I verify it's true
Adding another alias is fine if it has been used somewhere for the same concept. In that case, we should put a note at the bottom mentioning the alternate name with reference.
T382 could be replaced by $R_0$ + normal + submetacompact $\implies$ Dieudonne complete, perhaps T386 we can replace with pseudocompact + Dieudonne complete $\implies$ compact
T382 could be replaced by R₀ + normal + submetacompact ⟹ Dieudonne complete
Wrong. See notes in https://www.ams.org/journals/proc/1973-040-02/S0002-9939-1973-0322812-9/S0002-9939-1973-0322812-9.pdf, if measurable cardinality exists.
So I suggest add an extra weaker but correct theorem: R₁ + paracompact ⟹ Dieudonne complete (it can solve the unknown traits in pi-base now, though)
T386 we can replace with pseudocompact + Dieudonne complete ⟹ compact
This is right.
@prabau I've noticed there's no spaces which are $T_4$ and subparacompact, but not paracompact. I'm guessing those are equivalent?
@prabau I've noticed there's no spaces which are T 4 and subparacompact, but not paracompact. I'm guessing those are equivalent?
#742 is the counterexample. See https://scispace.com/pdf/on-subparacompact-spaces-2o1ji8yodk.pdf.
There is an exercise in Engelking referencing three papers, I assume one of them contains a somewhat easier proof of this
Oddly enough, I haven't found easy proof online, but I did find converse for GO-spaces