Real analysis: continuity

[lowasser]

Attempting to keep things general, I think we go:

1. Continuity of a function between metric spaces at a point (the function being defined in a neighborhood of the point)
2. Uniform continuity of a function between metric spaces
3. Extending a uniformly continuous function from Q to R to R to R

[lowasser]

#1375 addresses the first two of these. The third might not be possible without a choice principle?

HoTT says, "In general we do not expect [each Dedekind real to be the limit of a sequence of rational numbers] without further assumptions," and goes on to show that countable choice or excluded middle suffice.

It's not obvious to me, however, that constructing that sequence is a necessary condition. I'm confident that approximating the limit to an arbitrary positive rational epsilon requires a finite number of choices, and I think that might suffice.

[malarbol]

FWIW here's how TypeTopology addresses your third point; they don't seem to use any Cauchy approximation or sequence so it should be doable in our settings too. Our current definition of metric space is quite inspired in theirs, and with your recent work on distances functions and such, we should be able to readapt their proof in our settings.

[lowasser]

Marking this completed; I don't think we have the last bullet but I'm not actually a hundred percent sure it's true?

[malarbol]

Marking this completed; I don't think we have the last bullet but I'm not actually a hundred percent sure it's true?

I'm pretty sure it's true, and we have all the ingredients to transcribe the proof from https://martinescardo.github.io/TypeTopology/DedekindReals.Extension.html. There's still a lot of work involved, though. Or have you identified any obstruction in the proof?