Post #1888491

@jdw That's right. One way to think about it is that constructively it's consistent for R to 'not have enough points'. When this happens, if you take the join of the one-point sublocales of [0,∞), you get a proper sublocale of [0,∞). That said it's also not always going to be compatible with infinitary joins of open sublocales. If you have a singular cover of R, then there's a open proper sublocale of R that contains all of the points of R.