Cleanup for Noetherian and Alexandrov properties

[prabau]

Cleanup and a few tweaks for P208 (Noetherian) and P90 (Alexandrov).

In particular, for P90 removed the unnecessary word "unique" in "each point has a unique smallest neighborhood". That word was confusing people trying to prove that some spaces were Alexandrov, like in T826.

[Moniker1998]

@prabau why did you change T826?
Do you realize the difference between minimal element and minimum element? The argument there was important.

That proof was not a result of confusion, on the contrary.

[prabau]

That's exactly why I changed it.

As explained in the PR summary, the previous page for Alexandrov (P90) had "each point has a unique smallest neighborhood". Probably misled by the word "unique", Felix tried a few times, in some of the earlier commits in a PR, to justify the Alexandrov trait for some space, or a theorem like T826 maybe (don't remember exactly), by phrasing the argument like this:

"Suppose $U$ is a minimal open nbhd of $x$. blah blah blah Hence $U$ is unique."

But that is not quite a correct argument. One could imagine that in the poset of open nbhds of $x$, one has shown that there is indeed a single minimal element. But that is not enough, and it's not even useful. One really needs to show that minimal element is a minimum element. I.e., need to show $U$ is contained in every other nbhd of $x$.

That's why I removed the misleading "implying uniqueness of $U$ " at the end. As for the argument showing $U$ is minimum, of course this needs to be checked but it seemed kind of trivial and could be checked by the reader in their head. But if you really want, we can put that part back.

[prabau]

I have added some explanation for T826.

[prabau]

FYI, see this comment regarding a previous incorrect argument with "uniqueness": #1583 (comment)

[Moniker1998]

As for the argument showing U is minimum, of course this needs to be checked but it seemed kind of trivial and could be checked by the reader in their head. But if you really want, we can put that part back.

Yes this is exactly what I was referring to, and I don't think it's trivial, personally.