Add hereditary metaproperty for almost all properties which are

[felixpernegger]

Continuation of #1665.

I went over all properties (on spreadsheet) and noted which ones are hereditary and which ones are not.

The only ones remaining for which I do not know if they are hereditary or not are:

• P76 (probably not) not hereditary, see example 4 in https://www.sciencedirect.com/science/article/pii/S016686411400279X#se0060
• P101 (I would be surprised) Not hereditary. S192 minus natural numbers gives counterexample
• P120 (probably not, but hard to think of counterexample) not hereditary. See comments
• P138 (also doubt it, but pibase has only one nontrivial example for this property) Not hereditary, which (nontrivially) follow from Theorem 1.5 in https://arxiv.org/pdf/2211.12579
• P166 (likely no, because separable isnt hereditary) this is hereditary, following https://topology.pi-base.org/spaces?q=metrizable+%2B+Separable+%2B+%7EHereditarily+separable
• P169 (possibly? didnt wanna think about interiors in subspace topology too much) Not hereditary!!! One can take S185, it contains $\omega + 1$ with endpoint doubled.
• P173 (most likely no, since sequential isnt, but that was already annoying to find counterexample on the internet) not hereditary.
• P228 (no idea, also the most interesting case :) ) not hereditary, witnessed by S156, S23

If anyone wants to try, I used all easy tricks (locally 1-euclidean, ebeddable in R, empty space, singleton) already. A great amount of counterexamples for hard properties came from S108 and its subspaces in pi-base, maybe this also works for some of the remaing properties here.
Knowing that a property is NOT hereditary will be useful for a later proper implementation.

I was rather careful, but any metaproperty (positively) added in this PR should be checked (proofs should be all easy).

Again, the code itself was added by Claude Code based on my spreadsheet. :)

[prabau]

That may take a while to review properly. Any chance you could have a few smaller batches?

[felixpernegger]

That may take a while to review properly. Any chance you could have a few smaller batches?

I kind of prefer not to. Again, most of these are trivial (think: Hereditarily separable is hereditary)

[pzjp]

The example 2.5 in zbMATH 1458.54023 shows that P120 is not hereditary. If it was then it would actually be implied by P154.

[felixpernegger]

The example 2.5 in zbMATH 1458.54023 shows that P120 is not hereditary. If it was then it would actually be implied by P154.

thank you!!

[felixpernegger]

I keep this in draft until I figure out if the last 4 remaining properties are hereditary or not

[mathmaster13]

I keep this in draft until I figure out if the last 4 remaining properties are hereditary or not

I think this is the point. Even though we're pretty good at math, at least I am also pretty good at messing small but important things up. And so a reviewer of my PRs, as Patrick surely knows by this point, usually will find something that I've done incorrectly—even if the theorems are genuinely easy. Finding those small things is harder with larger PRs, I'd think.

[felixpernegger]

I keep this in draft until I figure out if the last 4 remaining properties are hereditary or not

I think this is the point. Even though we're pretty good at math, at least I am also pretty good at messing small but important things up. And so a reviewer of my PRs, as Patrick surely knows by this point, usually will find something that I've done incorrectly—even if the theorems are genuinely easy. Finding those small things is harder with larger PRs, I'd think.

It's much harder finding out properties are not hereditary. When they are hereditary, they prove is usually trivial. But in this PR, one only has to check those trivial ones.

I also tested with my tool from #1678 if any counterexamples for properties which I marked redundant are found, but nope.

[felixpernegger]

I went over all properties again (self-reviewed, so to say) and really the only tricky one is P166 (which isnt included yet)

[felixpernegger]

@prabau
I finally finished determining all the remaining properties.
Would be nice if this gets reviewed, since then we can add many traits very quickly (about 100).
The actual changes in this PR (saying what properties are hereditary) are almost very easy. So while a lot of files are changed, this shouldnt be too tricky to review.

Maybe we could also add to metaproperties when a property is not hereditary (this ought to be exactly not marked in this PR). This does not actually help the deduction, but may be useful for a reader?
Though finding counterexamples was much trickier than finding proofs for hereditary (I would have to go over all again probably to confirm)

[prabau]

Great. I'll start taking a look tomorrow.

Having a metaproperty declared (or deduced) either true or false for each property was the initial goal, given that we were going to have a more extensive change to the structure of the database. But since we don't have that, we only added the negative statements when they were surprising (e.g., semimetrizable vs. symmetrizable).
For now, I don't think we need to bother about the negative cases (and certainly not in this PR).