This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Topological definitions using the reals cncfcn1
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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion
cncfcn1 ⊢ ( ℂ –cn → ℂ ) = ( 𝐽 Cn 𝐽 )
Proof
Step
Hyp
Ref
Expression
1
cncfcn1.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2
ssid ⊢ ℂ ⊆ ℂ
3
1
cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
4
3
toponrestid ⊢ 𝐽 = ( 𝐽 ↾t ℂ )
5
1 4 4
cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn → ℂ ) = ( 𝐽 Cn 𝐽 ) )
6
2 2 5
mp2an ⊢ ( ℂ –cn → ℂ ) = ( 𝐽 Cn 𝐽 )