Description: Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 7-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cncfcn1.1 | |- J = ( TopOpen ` CCfld ) |
|
| Assertion | cncfcn1 | |- ( CC -cn-> CC ) = ( J Cn J ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cncfcn1.1 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | ssid | |- CC C_ CC |
|
| 3 | 1 | cnfldtopon | |- J e. ( TopOn ` CC ) |
| 4 | 3 | toponrestid | |- J = ( J |`t CC ) |
| 5 | 1 4 4 | cncfcn | |- ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( J Cn J ) ) |
| 6 | 2 2 5 | mp2an | |- ( CC -cn-> CC ) = ( J Cn J ) |