Negative result in Meta-properties?

[prabau]

Following the discussion in #1071, we have started adding a Meta-properties section at the bottom of some of the property pages. Example: https://topology.pi-base.org/properties/P000109, and others to follow. That is in particular useful when the meta-property is used in proofs of theorems or traits for spaces. E.g., that a certain property is hereditary.

What about also mentioning for example when a property is not hereditary? E.g., the fact that "symmetrizable" is not a hereditary property.

This is not a result that would used in proofs of anything else in pi-base. But it is maybe a surprising result and seems would be instructive to mention, giving an example illutrating this. (No more than one example needed.) In this case, with the Arens space and its subspace the Arens-Fort space. So we could have a meta-property entry like this:

- This property is not hereditary. (Example: {S72|P104} and {S23|P104})

with the curly brace directives expanding to the right thing.

It's deviating from the strict previous theorem/trait emphasis of pi-base though. What are your opinions about the idea?

@StevenClontz @GeoffreySangston @pzjp @yhx-12243 @david20000813 @danflapjax and others

[GeoffreySangston]

So would the idea be to only include this line whenever it seems interesting enough to pi-base editors, or would the idea be to try to include a line for each meta-property (e.g. hereditary or ~hereditary) for every property?

[david20000813]

I think this is a good idea, but it should be restricted only to cases that are surprising. Say, I don’t think it’s interesting to add normal is not hereditary, or compact is not hereditary. (Nor, for that matter, do I think we should add positive results that are just standard facts, say, $T_2$ is hereditary or metrizable is hereditary.)

For the specific case of symmetrizability, I do think adding it is not hereditary is interesting. We should probably also add semimetrizable is hereditary and maybe link them to each other to emphasize the contrast.

[prabau]

Not sure about the linking part though, especially in a tight meta-properties list. There are already so much of that. In this case, the meta-property of the other property is just a click away from the same page.

But only adding negative such results for "surprising" cases makes sense to me.

Would like to get @StevenClontz 's opinion too.

[david20000813]

@prabau I was suggesting linking the two mostly because the surprise in symmetrizable not being hereditary is, to me, more or less because semimetrizable is hereditary. It could be just a remark, like, “compare with P102, which is hereditary”. Though, of course, this depends on exactly how much space we’re working with.

[StevenClontz]

So would the idea be to only include this line whenever it seems interesting enough to pi-base editors

This, I think. Rather than a hard-defined rule, I think at this stage it can be the call of the editors whether the meta-property (true or false) is interesting enough to be included.

[prabau]

Thanks for the guidance everyone. I'll do a PR specifically for the examples discussed above.

Closing this for now.

[prabau]

Nor, for that matter, do I think we should add positive results that are just standard facts, say, T 2 is hereditary or metrizable is hereditary.

One last comment. I think it's fine for now. In the future, if we ever get to a more sophisticated deduction engine that can make wider use of meta-properties, we can revisit this.