adding examples to deduced non properties

[chadnash]

I wonder if specific counter examples might be useful when you ( non trivially :-) ) deduce that a property is not present for a topology.
for example in the deduced statement that the double origin topology (https://topology.pi-base.org/spaces/S000066) is not regular (https://topology.pi-base.org/spaces/S000066/properties/P000011) might include a specific closed set and point that cant be separate by disjoint open sets. For example:
the closed set C={(x,y): y<=0 or x^2 + y ^2 >=1} U {0} cannot be so separated from 0* .

may be also include the simple proof of this

[prabau]

This could be debatable. There may be some value in it in some cases. On the other hand, in this particular example, there is basically only one illustrating example for the non-regularity of the space, which is the one you gave. If it is straightforward, I would say this is a good "exercise for the user" to double check it for themselves if they are interested in that property. They will learn more by thinking about it themselves, given that the statement in question is already confirmed by combinations of various theorems in pi-base. This also reduces the clutter of trait files in pi-base.

Actually the same kind of issue applies when deducing that a certain property is true for a given space. Sometimes the deduction of that follows from a rather long and non-trivial graph of implications. And on the other hand, there could be a more direct argument giving a simpler proof of the result. We have usually chosen the path of not providing a simpler proof even if the result is deduced from some more complicated theorems. But that could be debated also.

Let's see what other maintainers think about this.

[StevenClontz]

I wouldn't mind having "annotated" deductions in the future. E.g. if we can deduce S123 has P456, one can still create the S123/P456 file to add some context/references without losing the deduction. (Maybe this should be the behavior when the value is unset on that file - then we could even add information on a property whose value may depend on your model of set theory.)

But for now, I think deductions are better than manual assertions (especially when they're just "look at this reference"), and users who want more details can discuss them on other forums such as Math.Stackexchange.