Description: Extension by continuity. Theorem 1 of BourbakiTop1 p. I.57. Given a topology J on C , a subset A dense in C , this states a condition for F from A to a regular space K to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cnextf.1 | |
|
cnextf.2 | |
||
cnextf.3 | |
||
cnextf.4 | |
||
cnextf.5 | |
||
cnextf.a | |
||
cnextf.6 | |
||
cnextf.7 | |
||
cnextcn.8 | |
||
Assertion | cnextcn | |