Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I gave continuous map a little bit of substance by giving it an actual Idea-paragraph and by writing out the epsilontic definition for the case of metric spaces, together with its equivalence to the “abstract” definition in terms of opens.
I added the nonstandard definition, largely because it makes precise an intuitive version that can go in the Idea section.
Something should be said about continuity at a point, but I don't have time to do that right now.
Another way to make precise the “preservation of closeness” is in terms of closeness to sets: if means that belongs to the closure of (a relation in terms of which the notion of topological space can equivalently be defined, at least in classical mathematics), then is continuous iff implies .
True, and of course that's directly related to the stuff you've been doing with proximity and apartness spaces.
I added to continuous map Frank Waaldijk’s very nice negative result that in constructive mathematics (by which I mean the kind of mathematics possible in a topos with natural numbers object) it cannot be shown that there is a notion of continuity of set-theoretic functions such that certain natural desiderata hold.
That result is already listed at fan theorem (since the existence of such a notion is equivalent to the fan theorem). Which is not to say that it should not also be listed at continuous map, of course.
I added some remarks beforehand about the different notions of continuity in constructive analysis.
Also, the problem is not so much that a kontinuous function on might not be bounded (since a uniformly continuous function must be bounded, even without the Fan Theorem, and it is specified that kontinuous functions on are uniformly continuous) but that a kontinuous, positive-valued function on might not be bounded below by a positive number (so that its reciprocal could not be bounded above, hence could not itself be kontinuous). So I rephrased that bit.
Toby, is there a significance to spelling it ’kontinuous’?
I presume that Waaldijk used a nonstandard spelling because he was speaking about an arbitrary set (with given properties) of partial functions while wanting to invoke a sense that these were more or less the continuous functions.
1 to 11 of 11