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

Definition df-cvm 29540
 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 29539 . 2 CovMap
2 vc . . 3
3 vj . . 3
4 ctop 19684 . . 3
5 vx . . . . . . . 8
6 vk . . . . . . . 8
75, 6wel 1843 . . . . . . 7
8 vs . . . . . . . . . . . 12
98cv 1404 . . . . . . . . . . 11
109cuni 4190 . . . . . . . . . 10
11 vf . . . . . . . . . . . . 13
1211cv 1404 . . . . . . . . . . . 12
1312ccnv 4821 . . . . . . . . . . 11
146cv 1404 . . . . . . . . . . 11
1513, 14cima 4825 . . . . . . . . . 10
1610, 15wceq 1405 . . . . . . . . 9
17 vu . . . . . . . . . . . . . . 15
1817cv 1404 . . . . . . . . . . . . . 14
19 vv . . . . . . . . . . . . . . 15
2019cv 1404 . . . . . . . . . . . . . 14
2118, 20cin 3412 . . . . . . . . . . . . 13
22 c0 3737 . . . . . . . . . . . . 13
2321, 22wceq 1405 . . . . . . . . . . . 12
2418csn 3971 . . . . . . . . . . . . 13
259, 24cdif 3410 . . . . . . . . . . . 12
2623, 19, 25wral 2753 . . . . . . . . . . 11
2712, 18cres 4824 . . . . . . . . . . . 12
282cv 1404 . . . . . . . . . . . . . 14
29 crest 15033 . . . . . . . . . . . . . 14 t
3028, 18, 29co 6277 . . . . . . . . . . . . 13 t
313cv 1404 . . . . . . . . . . . . . 14
3231, 14, 29co 6277 . . . . . . . . . . . . 13 t
33 chmeo 20544 . . . . . . . . . . . . 13
3430, 32, 33co 6277 . . . . . . . . . . . 12 t t
3527, 34wcel 1842 . . . . . . . . . . 11 t t
3626, 35wa 367 . . . . . . . . . 10 t t
3736, 17, 9wral 2753 . . . . . . . . 9 t t
3816, 37wa 367 . . . . . . . 8 t t
3928cpw 3954 . . . . . . . . 9
4022csn 3971 . . . . . . . . 9
4139, 40cdif 3410 . . . . . . . 8
4238, 8, 41wrex 2754 . . . . . . 7 t t
437, 42wa 367 . . . . . 6 t t
4443, 6, 31wrex 2754 . . . . 5 t t
4531cuni 4190 . . . . 5
4644, 5, 45wral 2753 . . . 4 t t
47 ccn 20016 . . . . 5
4828, 31, 47co 6277 . . . 4
4946, 11, 48crab 2757 . . 3 t t
502, 3, 4, 4, 49cmpt2 6279 . 2 t t
511, 50wceq 1405 1 CovMap t t
 Colors of variables: wff setvar class This definition is referenced by:  fncvm  29541  iscvm  29543
 Copyright terms: Public domain W3C validator