P110: Developable property

[prabau]

New P110 (Developable) and associated P113 (Moore space).
This may be useful when introducing the $G_\delta$-diagonal property.

As part of the change, T615 (metrizable => semimetrizable) is being replaced by
(developable + T0 => semimetrizable).

[prabau]

@pzjp This PR asserts that S74 (Niemytzki plane) is developable. One can then derive that it is semimetrizable (P102), and that trait could be removed.

But the explanation for P102 was pretty nice and it would be a shame to lose this direct verification. Before we remove it, we could move that to a mathse post to keep it for posterity. You could either write a question+answer combined, or one of us could ask a question and you could answer. What do you think?

[pzjp]

I can post my construction as an answer. I've got most of my pi-Base proofs saved, so it would be no problem it it gets removed from the site before.

[yhx-12243]

I can post my construction as an answer. I've got most of my pi-Base proofs saved, so it would be no problem it it gets removed from the site before.

Also something offtopic, GitHub (or git) can save the full history, so anyone with some git technology can retrieve the historical data easily.

[prabau]

@pzjp @yhx-12243
@StevenClontz @danflapjax: you may also be interested in the discussion below, which fits with some of your previous observations.

(T615) T0 developable spaces are semimetrizable. Since semimetrizable spaces are first countable and G_delta spaces, it follows that T0 developable spaces have both of these properties.

But developable, first countable, and G_delta space are properties that hold iff they hold in the Kolmogorow quotient.
So with a more powerful deduction system, it would automatically follow that developable spaces are first countable and G_delta spaces, even without T0.

In particular, we would not need (T710) developable => first countable.
I added T710 explicitly because it seemed an easy way to deduce a lot of traits (for developable = false).

I did not add [developable => G_delta]. Maybe we should? At least, it does not seem to be needed to derive any additional traits at the moment.

All of this, because "semimetrizable" requires T0. (It's like "pseudometrizable" vs. "metrizable".) If there was a version of "semimetrizable" with only half of the reflexivity condition, something like "pseudo-semimetrizable", things would be simpler. (disclaimer: I am not advocating adding this). Really better would be a more powerful deduction system.

Thoughts?

[prabau]

@pzjp @yhx-12243 Would one of you be interested in reviewing this?

[pzjp]

Haven't found any issue.
Also cannot access Willard's book to check citation.

[prabau]

Also cannot access Willard's book to check citation.

If you want, I can post of a picture of that page.

[prabau]