Continuing (and improving) #1753.
- Locally euclidean + toronto => discrete:
Proof: Suppose some point x is not isolated, i.e. has R^n for n>0 as nbhd. Then essentially take out a sequence congerving (but not containing x), the resulting space has same card as original, but isnt locally euclidean at x anymore.
- Locally Finite + Toronto + ~Finite => Has an isolated point.
Proof: Suppose x is not isolated; take some finite nbhd and remove all points in that nbhd except x. Assertion follows with Toronto.
- Has a generic point + Toronto + ~Indiscrete + ~Finite => Has an isolated point
Proof: Suppose X is infinite. Let A be the set of generic points. If |A|= |X|, X were indiscrete, else 1+|X/A| = |X|, so X must have exactly one generic point p. So X/p has another generic point q. But q isnt generic in X, so p must be isolated.
- Has a point with a unique nbhd + Toronto + ~indicsrete + ~finite => Has a closed point
Proof: Mirror the proof in 3).
- Locally Countable + Toronto + ~Countable => Has an isolated point.
Proof: Mirror the proof in 2)
Continuing (and improving) #1753.
Proof: Suppose some point x is not isolated, i.e. has R^n for n>0 as nbhd. Then essentially take out a sequence congerving (but not containing x), the resulting space has same card as original, but isnt locally euclidean at x anymore.
Proof: Suppose x is not isolated; take some finite nbhd and remove all points in that nbhd except x. Assertion follows with Toronto.
Proof: Suppose X is infinite. Let A be the set of generic points. If |A|= |X|, X were indiscrete, else 1+|X/A| = |X|, so X must have exactly one generic point p. So X/p has another generic point q. But q isnt generic in X, so p must be isolated.
Proof: Mirror the proof in 3).
Proof: Mirror the proof in 2)