Theorem Suggestion: Sequential implies Ascoli

[konradvoelkel]

Theorem Suggestion

If a space is:

• P79

then it is P85.

Rationale

This theorem would demonstrate that no spaces satisfy the following search:

https://topology.pi-base.org/spaces?q=Sequential+%26+%7E+Ascoli

Proof/References

The result is stated without proof in Gabriyelyan et. al. "The Ascoli property for function spaces". A quick proof goes by showing sequential => k-space (which is fairly straightforwards) and k-space => Ascoli, which is the classical Ascoli Theorem from Engelking, General Topology 1989, 3.4.20.

Comment

It would probably better to include the Property "k-space" and add two theorems, and also hunt for a better reference of sequential => k-space (of which there are many proofs to be found by quickly googling already). I found it odd that the property "Ascoli" exists without any theorems or spaces attached to it. This made it "unknown" wheter the two-element discrete space has this property, and adding this theorem would fix that (the space is indeed Ascoli). The whole area of maths seems to have abundant implications with counterexamples for the counterdirection, so it's nice fit for this project.

[Moniker1998]

https://www.sciencedirect.com/science/article/pii/S0166864116302152

Compactly generated => Ascoli

This is a stronger theorem so should be included rather than what you are proposing

[konradvoelkel]

Ah, I found now the k-space property as P140 so there should be both sequential => P140 as well as P140 => Ascoli

I didn't find it first because I was looking for "k-space" instead of "$k$-space". Maybe on the UX side this can be improved (by stating clearly that $ is encouraged or even a more fuzzy search), but that is an entirely other issue.

[prabau]

Thanks for your suggestions. At the moment the Ascoli property is just a placeholder without any theorems or example spaces. We plan to flesh this out at some point and we'll definitely incorporate your suggested theorems as part of that.

As for k-spaces/compactly generated spaces, there are are actually three variants, to accommodate the variations in definitions in the literature: $k_3$-space (P142) ==> $k_2$-space (P141) ==> $k_1$-space (P140). Which one of the k-space properties is the one that would fit in your suggestion?

As for searching by property name, note that each of the k-space variants has k-space without dollar signs as an alias. Also, the search feature of the pi-base web interface already uses fuzzy matching. So for example when I enter k-space in the search box in the property page (https://topology.pi-base.org/properties?filter=k-space), it lists the three properties as the first three choices. Same thing when entering k-space in the Filter by Formula box in the Explore page.

[Moniker1998]

The article I've posted above seems to consider Tychonoff spaces $X$, while the original article that defines Ascoli spaces seems to consider $T_3$ spaces.

So, what separation properties do we require from Ascoli spaces, if any?