Maybe it's worth mentioning that US is equivalent to "every sequentially compact subset is sequentially closed"

[Jianing-Song]

This is analogous to KC = "every compact subset is closed".

Proof: Suppose that $X$ is US. Let $C$ be a sequentially compact subset of $X$, then there is no sequence in $C$ converging to a point outside $C$, otherwise this sequence has a subsequence converging to a point in $C$ by sequential compactess, and we get a sequence with two different limits.

Conversely, suppose that every sequentially compact subset is sequentially closed. Each singleton is sequentially compact, hence sequentially closed, which implies that $X$ is $T_1$. Suppose that there is a sequence $(x_n)$ converging to both $a\neq b$. By taking the open neighborhood $U=X\setminus{b}$ of $a$ we see that $x_n\neq b$ for all sufficiently large $n\ge N$, and $(xn){n\ge N}\cup{a}$ that is not sequentially closed ($b$ is in its sequential closure).

[StevenClontz]

I think this is a good perspective to add, but is this result in the literature or a forum like Math.StackExchange that we can cite? We generally want the results we include in the pi-Base to be aired out more widely than our GitHub.

[StevenClontz]

If it's not somewhere citable, I'm happy to ask the question on Math.StackExchange for @Jianing-Song to answer.

[Jianing-Song]

I assume you meant KC = "every compact subset is closed" ?

Yes, sorry for the typo. Corrected.

[prabau]

@Jianing-Song This result is an interesting observation. Whether it fits as a "pi-base theorem" is another question. As you have seen, the information in pi-base consist of a list of properties, a list of theorems and a list of spaces. The properties are unique up to equivalence. The theorems are of the form [some set of properties or their negation ==> some property/its negation]. Now in topology there are many results that do not fit into this mold, and hence do not fit into pi-base.

At the most, since the new property "every sequentially compact subset is sequentially closed" is equivalent to US, it could possibly be mentioned as a sentence in US. But even that could be debatable. Some properties are described with several equivalent definitions. For example, Baire or Alexandrov or ... But these the equivalent defs are usually semantically close to one another. So I am not sure in this case. We should discuss further.

[Jianing-Song]

@Jianing-Song This result is an interesting observation. Whether it fits as a "pi-base theorem" is another question. As you have seen, the information in pi-base consist of a list of properties, a list of theorems and a list of spaces. The properties are unique up to equivalence. The theorems are of the form [some set of properties or their negation ==> some property/its negation]. Now in topology there are many results that do not fit into this mold, and hence do not fit into pi-base.

At the most, since the new property "every sequentially compact subset is sequentially closed" is equivalent to US, it could possibly be mentioned as a sentence in US. But even that could be debatable. Some properties are described with several equivalent definitions. For example, Baire or Alexandrov or ... But these the equivalent defs are usually semantically close to one another. So I am not sure in this case. We should discuss further.

Yes, I understand this situation. Thanks!

[StevenClontz]

@prabau yeah, I was viewing this as an edit to US's description, not a new property. But we need a citation for it outside our GitHub.