Description: An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | blsconn.j | |
|
blsconn.s | |
||
blsconn.k | |
||
Assertion | blsconn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | blsconn.j | |
|
2 | blsconn.s | |
|
3 | blsconn.k | |
|
4 | cnxmet | |
|
5 | blssm | |
|
6 | 4 5 | mp3an1 | |
7 | 2 6 | eqsstrid | |
8 | 2 | blcvx | |
9 | 7 8 1 3 | cvxsconn | |