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)
• P101 (I would be surprised)
• 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)
• P166 (likely no, because separable isnt hereditary) this is hereditary, following https://topology.pi-base.org/spaces?q=metrizable+%2B+Separable+%2B+%7EHereditarily+separable (havent added this in the pr yet)
• P169 (possibly? didnt wanna think about interiors in subspace topology too much)
• 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.