More spaces that are locally a half-line

[prabau]

Some more spaces that are locally a half-line:

• S158: interval [0,1]
• S210: interval [0,1)
• S38: long ray

[felixpernegger]

One small suggestion, but either way is fine

[felixpernegger]

Suggested change

	By inspection.
	Evident from the definitions.

This is close to what we usually write? If you dont like it, just ignore

[GeoffreySangston]

Fun fact. Looks like we have 55 instances of "Evident from the definition" and 20 instances of "Follows from the definition".

[prabau]

We have some other variants too.

Here I wanted to indicate that one has to inspect the space, i.e., look at it in some amount of detail. Hence "by inspection". So I will leave it the way it is.

[prabau]

There is also "Immediate from the definition" (32 instances).

[felixpernegger]

smart :)

[prabau]

Note: For S38 (long ray), P200 (simply connected) looks like it would become redundant. But I did not remove it, because the explicit justification is is needed for T850 (LOTS + path connected => simply connected). Without it, there would be a circular dependency.

[felixpernegger]

Note: For S38 (long ray), P200 (simply connected) looks like it would become redundant. But I did not remove it, because the explicit justification is is needed for T850 (LOTS + path connected => simply connected). Without it, there would be a circular dependency.

Maybe it would be good to keep on list (not necessarily on the website) of manual traits which must not be removed (because they are used for theorems etc)