Description: A mapping is continuous at P in a first-countable space X iff it is sequentially continuous at P , meaning that the image under F of every sequence converging at P converges to F ( P ) . This proof uses ax-cc , but only via 1stcelcls , so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 1stccnp.1 | |
|
1stccnp.2 | |
||
1stccnp.3 | |
||
1stccnp.4 | |
||
Assertion | 1stccnp | |