Closed david20000813 closed 1 day ago
One additional comment here: should we delete T135, Completely metrizable => Baire, since it now follows from T133, Completely metrizable => Čech-complete, and the proposed T623, Čech-complete => Baire?
Often in this case we will edit T135 rather than introduce a new T623.
@StevenClontz I'll do that then.
It's more than just "asserted" in the referenced theorems. Better say See Theorem ...
.
For T623: the $k_3$-space property is the least useful of the three variants of $k$-space in general. Better use $k_1$-space (P140). It's all the same anyway for Hausdorff spaces.
@prabau The reason I used $k_3$ is because it is the strongest among all $k$-space properties. In particular, it implies $k_2$ then $k_1$. Also why I chose $k_1$ in #944, where asserting not $k_1$ is the strongest available property. Though, of course, we're talking about Hausdorff spaces here, so it really doesn't matter. It just feels better to assert what formally is the strongest possible conclusion.
Yeah, I understand. But they are equivalent in this case. And practically nobody uses k3-space in the literature. We introduced it in pi-base to better distinguish the various variants in the definitions. k1-space is easier to check than the rest in this case. So I will really insist here.
You can also compare the variants in https://en.wikipedia.org/wiki/Compactly_generated_space (CG3/Def 3 does not have good properties in general.)
@prabau In that case, sure, I've changed the theorem to imply $k_1$ instead.
One additional argument in favor of k1 in this case: the proof in Engelking shows k1 and not k3. Again, they are all equivalent, but k1 is the more natural and simpler version when working with Hausdorff spaces. k3 is more a strengthening of k2 used to illustrate the reason for the k2 definition, via the shortcomings of k3.
One additional comment here: should we delete T135, Completely metrizable => Baire, since it now follows from T133, Completely metrizable => Čech-complete, and the proposed T623, Čech-complete => Baire?
See #930.