Last month I found out that there are in fact discontinuous partial functions on ℝ. For example, on the domain D ≝ {x:ℝ | x < 0 ∨ 0 ≤ x} one can define the function f where f(x) = -1 for x < 0 and f(x) = 1 for 0 ≤ x. One can prove that this function is discontinuous using the topology of ℝ.
Classically D = ℝ, but constructively one can only prove D ⊆ ℝ. For example consider y = ∑i : ℕ ai2-i where ai = -1 if the aith proof in one’s system proves false, and ai = 0 otherwise. It is easy to prove this sum must converge, so y ∈ ℝ; however, if one could constructively prove y ∈ D then one could prove y < 0 or one could prove 0 ≤ y. In either case the result would mean the system is inconsistent.
I had thought that all partial functions on ℝ were continuous, and rather than use discontinuous functions one would use the functions with the discontinuous points removed. Apparently I was wrong.
Note that the function f is continuous using the natural topology of the representatives of its domain. Also note that one cannot prove there are any discontinuous functions whose domain is all of ℝ.