Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | limccnp2.r | |
|
limccnp2.s | |
||
limccnp2.x | |
||
limccnp2.y | |
||
limccnp2.k | |
||
limccnp2.j | |
||
limccnp2.c | |
||
limccnp2.d | |
||
limccnp2.h | |
||
Assertion | limccnp2 | |