Post #1733539
2026-04-26 20:32 UTC
Question: Constructively, the real line is not covered by (-oo,0] and [0, oo) because for a given real number one can't decide if it's <=0 or >=0. Does the locale of real numbers fix this somehow? Are there two closed sublocales (-oo,0] and [0,oo) whose join is R?
Followup question: Does this allow to define a real function (as a map of locales) which is =0 on (-oo,0] and exp(-1/x) on [0,oo) constructively? (This is the function usually used to prove existence of bump functions https://en.wikipedia.org/wiki/Non-analytic_smooth_function)
Probably not, because I guess everything would descend to the topological space.
Replies (1)
-
@jameshanson@mathstodon.xyz 2026-04-26 21:31
@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.