Post #1888489

@jdw The answer to your first question should be yes since it's already the case that the join of (-∞,0) and [0,∞) in the lattice of sublocales of R is R. Regarding your followup question, it should be fairly easy to define this bump function constructively (on R as a locale and thereby on R as a topological space) since it's computable. More generally, you can constructively show that for any functions f : (-∞,0] → R and g : [0,∞) → R with the same limit at 0, there is a function h : R → R such that h(x) = f(x) for x ≤ 0 and h(x) = g(x) for x ≥ 0.