Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo . Since any ~>r limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrlimcnp.a | |
|
xrlimcnp.b | |
||
xrlimcnp.r | |
||
xrlimcnp.c | |
||
xrlimcnp.j | |
||
xrlimcnp.k | |
||
Assertion | xrlimcnp | |