pi-base
Mysior plane
Mysior plane, first defined by Mysior, is an example of a space that's union of two closed realcompact subspaces but which isn't realcompact. Definition can be found in this article as example 5. The original article can be found here but I'm not sure if anyone is able to access it.
I proved that this space is Tychonoff and upper/lower half-planes are realcompact here As shown in this article, if Mysior plane were normal then it'd union of two z-embedded realcompact subspaces, so realcompact. This contradicts that it isn't realcompact. So the Mysior plane is not normal
The property realcompact is not currently tracked by pi-base, so we have some steps to add it. https://github.com/pi-base/data/wiki/Contributing#requirements-for-a-new-property
Clearly this meets the first requirement of notability. So then we also prefere to have theorems establishing necessary and sufficient conditions, so we can automatically deduce whether many of our existing spaces are realcompact.
I propose Lindelof => realcompact (Engelking 3.11.12 p216) for one direction.
The other issue: Engelking assumes T_{3.5} throughout. We generally prefer to not assume separation axioms, but at least for a first pass we may need to add T_{3.5} as a necessary condition for our theorems.
I guess it depends on what we choose as definition for realcompact. If we go with Willard 17H (realcompact = can be embedded as a closed subset of a product of copies of the real line), such spaces must be Tychonoff (T3.5 is preserved by products and subspaces). What's the best definition for realcompact?
Also Engelking assume T3 (what he calls regular) as part of Lindelof, so will probably have to tweak that.
Perhaps the best case scenario would be to find a characterization for realcompact that results in the following cute result for T3.5 spaces without any (or many) separation assumptions:
compact <=> realcompact + pseudocompact
I've asked the question here: https://math.stackexchange.com/questions/4728863
I much prefer the Willard characterization compared with others I've seen, though it seems to obfuscate that it is a necessary condition for compact Hausdorff spaces (at least the proof doesn't jump out to me; I think that's maybe another interesting question to pose).
I also agree that Willard's definition looks nice, but when actually trying to prove that something is realcompact, it's mostly useless. I think that's why it's not as popular as the other equivalent definitions. Not only that, but there's a deep connection between realcompactness and continuous functions C(X) = C(X; R) which that definition doesn't clarify. By the way, I answered your question in the positive, we don't need T3.5 for this, and equivalence compact iff realcompact + pseudocompact holds.
There exist spaces which are Lindelof, pseudocompact and not compact, so we can't show that Lindelof implies realcompact without any assumptions.
https://topology.pi-base.org/spaces?q=lind%2Bpseudo%2B~compact%2BT2%2Bstrongly%20conn Examples like those are Strongly connected (= all continuous real valued functions are constant), which trivially implies pseudocompact.
With your proposed general definition of realcompact in terms of stable families, can a realcompact space ever be strongly connected (i.e. trivial C(X))? (unless it's the trivial case of a singleton X of course)
Yeah, indiscrete topology on any set is an example here. Such space needs to be compact of course, a space is strongly connected and realcompact iff it's compact strongly connected (since strongly connected implies pseudocompact).
A Tychonoff space X is easily seen to be strongly connected iff X has zero or one point. A strongly connected compact Hausdorff space needs to necessarily be Tychonoff, hence empty or singleton. However, there are examples of T_1 strongly connected compact spaces (e.g. S000029), as well as T_3 strongly connected spaces (S000090) which aren't of this form in pi-base.
Proof: If X is Tychonoff and strongly connected, then C(X) = R or C(X) = 0. Thus C(X) = C(uX) where uX is realcompactification of X. But noting that C(Y) = R for Y singleton and C(Y) = 0 for Y empty, since both of those are realcompact and C(uX) = C(Y), we have that uX and Y are homeomorphic, so X embedds into Y. So |X| is at most 1.
As far as which notion of realcompact we should use in pi-base, I think the best would be to use the classical one, as that's the one people are used to. So we can give the Willard characterization together with one or two convenient equivalent formulations (all implying Tychonoff).
Further generalizations could be introduced later on, if someone wanted to. But there are a whole slew of them and it's not clear which ones are better than others. See https://www.utm.edu/staff/jschomme/realcom.html and https://books.google.com.pe/books?id=JWyoCRkLFAkC&printsec=frontcover#v=onepage&q=realcompact&f=false (page 185)
A Tychonoff space X is easily seen to be strongly connected iff X has zero or one point.
Or let pi-base do the work: https://topology.pi-base.org/spaces?q=tychonoff%2Bstrongly%20conn%2Bhas%20distinct%20points (although it seems we need a minor fix in T114)
Because it's such a natural thing, I'll make a PR that adds Closed subspace of Euclidean space with the alias of realcompact. Then we can proceed with this request.
I'll try introducing more about realcompactness of spaces, including adding the Mysior plane, once the definition and basic theorems are here. For now it's postponed.
Great! And if you don't mind, let's do it step by step with small PRs at a time instead of a gigantic change. It will make things easier to review and incorporate.
I'll add the property of realcompactness to all the spaces which don't have it this week. Of course I'll group them into different pull requests so it's easier to check. Introduction of Mysior plane should probably be done after that