Long line (topology)
en.wikipedia.org
en.wikipedia.org
https://en.wikipedia.org/wiki/Lindel%C3%B6f_space
It is also not separable, i.e. no countable everywhere dense subset.
I've added this to the Wikipedia page.
Think about "talking a walk" along the Euclidean Line -- the real-number line, if you like. Face in one direction, and then start taking steps.
Stepping Example #1. Start at 0 and face toward the positive numbers. Step to 1. Step to 2. Step to 3. Step to 4. Etc. Each time you take a step, just a bit more of the line is behind you. And if I pick a point on the line, then no matter which point I pick, this way of stepping will eventually put that point behind you.
Stepping Example #2. Start at 0 and face toward the positive numbers. Step to 1/2. Step to 2/3. Step to 3/4. Step to 4/5. Etc. Again, each time you take a step, just a bit more of the line is behind you. But this time, I can find points -- 6, for example, or 300 million -- that will never be behind you.
(There is a technical term for the first kind of stepping. We say that the set of points you step on, is cofinal in the order on the Euclidean Line. The second kind of stepping does not have this property.)
One of the curious properties of the Long Line is, first, that "locally", it is exactly like the Euclidean Line. Stand anywhere on the Long Line and look around. "Looks like I'm on the Euclidean Line," you say. But, second, every possible way of stepping ends up like Example #2 above. No matter what steps you choose to take, I can find a point -- lots of points, in fact -- that will never be behind you.
And that is why we say it is "long".
(Formally, the Long Line is locally homeomorphic to the Euclidean Line, but the order on the Long Line admits no countable cofinal subset.)
And even if you know what all the words mean, it can take some time and effort to put them together, even for practitioners.
And even when you understand the concepts and ideas, it can still be difficult to understand the definitions. Few months ago, a professor told us the 100% formal definition of a function: it wasn't easy to understand and we all had this "wtf" face.
But the reason we write definitions as little programs to be compiled is to make sure that there can be no room for ambiguity. You compile the definition and arrive at the same mathematical object as anyone else. If we define a function as a mapping or a procedure, then we just shifted one word for another and still have to elucidate what a mapping or a procedure is.
Type theory gives a formal definition closer to the intuitive notion: a function from A to B is a program of type A -> B. I.e., a rule for turning things of type A into things of type B.
What's the book to read for this stuff?
It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like
"give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a".
As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good.
Chapter 1 gives the basics of dependent type theory.
Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice).
Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).