Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cvm Structured version   Unicode version

Definition df-cvm 24948
 Description: Define the class of covering maps on two topological spaces. A function is a covering map if it is continuous and for every point in the target space there is a neighborhood of and a decomposition of the preimage of as a disjoint union such that is a homeomorphism of each set onto . (Contributed by Mario Carneiro, 13-Feb-2015.)
Assertion
Ref Expression
df-cvm CovMap t t
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-cvm
StepHypRef Expression
1 ccvm 24947 . 2 CovMap
2 vc . . 3
3 vj . . 3
4 ctop 16963 . . 3
5 vx . . . . . . . 8
6 vk . . . . . . . 8
75, 6wel 1727 . . . . . . 7
8 vs . . . . . . . . . . . 12
98cv 1652 . . . . . . . . . . 11
109cuni 4017 . . . . . . . . . 10
11 vf . . . . . . . . . . . . 13
1211cv 1652 . . . . . . . . . . . 12
1312ccnv 4880 . . . . . . . . . . 11
146cv 1652 . . . . . . . . . . 11
1513, 14cima 4884 . . . . . . . . . 10
1610, 15wceq 1653 . . . . . . . . 9
17 vu . . . . . . . . . . . . . . 15
1817cv 1652 . . . . . . . . . . . . . 14
19 vv . . . . . . . . . . . . . . 15
2019cv 1652 . . . . . . . . . . . . . 14
2118, 20cin 3321 . . . . . . . . . . . . 13
22 c0 3630 . . . . . . . . . . . . 13
2321, 22wceq 1653 . . . . . . . . . . . 12
2418csn 3816 . . . . . . . . . . . . 13
259, 24cdif 3319 . . . . . . . . . . . 12
2623, 19, 25wral 2707 . . . . . . . . . . 11
2712, 18cres 4883 . . . . . . . . . . . 12
282cv 1652 . . . . . . . . . . . . . 14
29 crest 13653 . . . . . . . . . . . . . 14 t
3028, 18, 29co 6084 . . . . . . . . . . . . 13 t
313cv 1652 . . . . . . . . . . . . . 14
3231, 14, 29co 6084 . . . . . . . . . . . . 13 t
33 chmeo 17790 . . . . . . . . . . . . 13
3430, 32, 33co 6084 . . . . . . . . . . . 12 t t
3527, 34wcel 1726 . . . . . . . . . . 11 t t
3626, 35wa 360 . . . . . . . . . 10 t t
3736, 17, 9wral 2707 . . . . . . . . 9 t t
3816, 37wa 360 . . . . . . . 8 t t
3928cpw 3801 . . . . . . . . 9
4022csn 3816 . . . . . . . . 9
4139, 40cdif 3319 . . . . . . . 8
4238, 8, 41wrex 2708 . . . . . . 7 t t
437, 42wa 360 . . . . . 6 t t
4443, 6, 31wrex 2708 . . . . 5 t t
4531cuni 4017 . . . . 5
4644, 5, 45wral 2707 . . . 4 t t
47 ccn 17293 . . . . 5
4828, 31, 47co 6084 . . . 4
4946, 11, 48crab 2711 . . 3 t t
502, 3, 4, 4, 49cmpt2 6086 . 2 t t
511, 50wceq 1653 1 CovMap t t
 Colors of variables: wff set class This definition is referenced by:  fncvm  24949  iscvm  24951
 Copyright terms: Public domain W3C validator