This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = J Cn J$

Proof

Step	Hyp	Ref	Expression
1		cncfcn1.1	$⊢ J = TopOpen (ℂ_{fld})$
2		ssid	$⊢ ℂ \subseteq ℂ$
3	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
4	3	toponrestid	$⊢ J = J ↾_{𝑡} ℂ$
5	1 4 4	cncfcn	$⊢ (ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℂ = J Cn J$
6	2 2 5	mp2an	$⊢ ℂ \underset{cn}{⟶} ℂ = J Cn J$