Description: Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-sconn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csconn | |
|
1 | vj | |
|
2 | cpconn | |
|
3 | vf | |
|
4 | cii | |
|
5 | ccn | |
|
6 | 1 | cv | |
7 | 4 6 5 | co | |
8 | 3 | cv | |
9 | cc0 | |
|
10 | 9 8 | cfv | |
11 | c1 | |
|
12 | 11 8 | cfv | |
13 | 10 12 | wceq | |
14 | cphtpc | |
|
15 | 6 14 | cfv | |
16 | cicc | |
|
17 | 9 11 16 | co | |
18 | 10 | csn | |
19 | 17 18 | cxp | |
20 | 8 19 15 | wbr | |
21 | 13 20 | wi | |
22 | 21 3 7 | wral | |
23 | 22 1 2 | crab | |
24 | 0 23 | wceq | |