Home Metamath Proof ExplorerTheorem List (p. 233 of 315) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21493) Hilbert Space Explorer (21494-23016) Users' Mathboxes (23017-31457)

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcvmsrcl 23201* Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsi 23202* One direction of cvmsval 23203. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsval 23203* Elementhood in the set of all even coverings of an open set in . is an even covering of if it is a nonempty collection of disjoint open sets in whose union is the preimage of , such that each set is homeomorphic under to . (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsss 23204* An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsn0 23205* An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsuni 23206* An even covering of has union equal to the preimage of by . (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsdisj 23207* An even covering of is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t

Theoremcvmshmeo 23208* Every element of an even covering of is homeomorphic to via . (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsf1o 23209* , localized to an element of an even covering of , is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t        CovMap

Theoremcvmscld 23210* The sets of an even covering are clopen in the subspace topology on . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t        CovMap t

Theoremcvmsss2 23211* An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
t t        CovMap

Theoremcvmcov2 23212* The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
t t        CovMap

Theoremcvmseu 23213* Every element in is a member of a unique element of . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t               CovMap

Theoremcvmsiota 23214* Identify the unique element of containing . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmopnlem 23215* Lemma for cvmopn 23217. (Contributed by Mario Carneiro, 7-May-2015.)
t t               CovMap

Theoremcvmfolem 23216* Lemma for cvmfo 23237. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t                      CovMap

Theoremcvmopn 23217 A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmliftmolem1 23218* Lemma for cvmliftmo 23221. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally                                           t t                             t

Theoremcvmliftmolem2 23219* Lemma for cvmliftmo 23221. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally                                           t t

Theoremcvmliftmoi 23220 A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally

Theoremcvmliftmo 23221* A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.)
CovMap               𝑛Locally

Theoremcvmliftlem1 23222* Lemma for cvmlift 23236. In cvmliftlem15 23235, we picked an large enough so that the sections are all contained in an even covering, and the function enumerates these even coverings. So is a neighborhood of , and is an even covering of , which is to say a disjoint union of open sets in whose image is . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem2 23223* Lemma for cvmlift 23236. is a subset of for each . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem3 23224* Lemma for cvmlift 23236. Since is a neighborhood of , every element satisfies . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem4 23225* Lemma for cvmlift 23236. The function will be our lifted path, defined piecewise on each section for . For , it is a "seed" value which makes the rest of the recursion work, a singleton function mapping to . (Contributed by Mario Carneiro, 15-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem5 23226* Lemma for cvmlift 23236. Definition of at a successor. This is a function defined on as where is the unique covering set of that contains evaluated at the last defined point, namely (note that for this is using the seed value ). (Contributed by Mario Carneiro, 15-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem6 23227* Lemma for cvmlift 23236. Induction step for cvmliftlem7 23228. Assuming that is defined at and is a preimage of , the next segment is also defined and is a function on which is a lift for this segment. This follows explicitly from the definition since is in for the entire interval so that maps this into and maps back to . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem7 23228* Lemma for cvmlift 23236. Prove by induction that every function is well-defined (we can immediately follow this theorem with cvmliftlem6 23227 to show functionality and lifting of ). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem8 23229* Lemma for cvmlift 23236. The functions are continuous functions because they are defined as where is continuous and is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap                                                                       t

Theoremcvmliftlem9 23230* Lemma for cvmlift 23236. The functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem10 23231* Lemma for cvmlift 23236. The function is going to be our complete lifted path, formed by unioning together all the functions (each of which is defined on one segment of the interval). Here we prove by induction that is a continuous function and a lift of by applying cvmliftlem6 23227, cvmliftlem7 23228 (to show it is a function and a lift), cvmliftlem8 23229 (to show it is continuous), and cvmliftlem9 23230 (to show that different functions agree on the intersection of their domains, so that the pasting lemma paste 17017 gives that is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap                                                                       t        t

Theoremcvmliftlem11 23232* Lemma for cvmlift 23236. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem13 23233* Lemma for cvmlift 23236. The initial value of is because is a subset of which takes value at . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem14 23234* Lemma for cvmlift 23236. Putting the results of cvmliftlem11 23232, cvmliftlem13 23233 and cvmliftmo 23221 together, we have that is a continuous function, satisfies and , and is equal to any other function which also has these properties, so it follows that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem15 23235* Lemma for cvmlift 23236. Discharge the assumptions of cvmliftlem14 23234. The set of all open subsets of the unit interval such that is contained in an even covering of some open set in is a cover of by the definition of a covering map, so by the Lebesgue number lemma lebnumii 18459, there is a subdivision of the unit interval into equal parts such that each part is entirely contained within one such open set of . Then using finite choice ac6sfi 7096 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 23234. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmlift 23236* One of the important properties of covering maps is that any path in the base space "lifts" to a path in the covering space such that , and given a starting point in the covering space this lift is unique. The proof is contained in cvmliftlem1 23222 thru cvmliftlem15 23235. (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmfo 23237 A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmliftiota 23238* Write out a function that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmlift2lem1 23239* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)

Theoremcvmlift2lem9a 23240* Lemma for cvmlift2 23253 and cvmlift3 23265. (Contributed by Mario Carneiro, 9-Jul-2015.)
t t        CovMap                                                                t

Theoremcvmlift2lem2 23241* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem3 23242* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem4 23243* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem5 23244* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem6 23245* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap                                           t

Theoremcvmlift2lem7 23246* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem8 23247* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 9-Mar-2015.)
CovMap

Theoremcvmlift2lem9 23248* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                                    t        t                                    t               t

Theoremcvmlift2lem10 23249* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                      t t

Theoremcvmlift2lem11 23250* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                                                              t t

Theoremcvmlift2lem12 23251* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem13 23252* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2 23253* A two-dimensional version of cvmlift 23236. There is a unique lift of functions on the unit square which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmliftphtlem 23254* Lemma for cvmliftpht 23255. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmliftpht 23255* If and are path-homotopic, then their lifts and are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmlift3lem1 23256* Lemma for cvmlift3 23265. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem2 23257* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem3 23258* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem4 23259* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem5 23260* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem6 23261* Lemma for cvmlift3 23265. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                                                       t

Theoremcvmlift3lem7 23262* Lemma for cvmlift3 23265. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                    t PCon

Theoremcvmlift3lem8 23263* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3lem9 23264* Lemma for cvmlift2 23253. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3 23265* A general version of cvmlift 23236. If is simply connected and weakly locally path-connected, then there is a unique lift of functions on which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

18.4.10  Undirected multigraphs

Syntaxcumg 23266 Extend class notation with undirected multigraphs.
UMGrph

Syntaxceup 23267 Extend class notation with Eulerian paths.
EulPaths

Syntaxcvdg 23268 Extend class notation with the vertex degree function.
VDeg

Definitiondf-umgra 23269* Define the class of all undirected multigraphs. A multigraph is a pair where is a function into subsets of of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Definitiondf-eupa 23270* Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths UMGrph

Definitiondf-vdgr 23271* Define the vertex degree function for an undirected multigraph. We have to double-count those edges that contain "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremrelumgra 23272 The class of all undirected multigraphs is a relation. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremisumgra 23273* The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremwrdumgra 23274* The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)
Word UMGrph Word

Theoremumgraf2 23275* The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph

Theoremumgraf 23276* The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgrass 23277 An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgran0 23278 An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgrale 23279 An edge has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgrafi 23280 An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgraex 23281* An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)
UMGrph

Theoremumgrares 23282 A subgraph of a graph (formed by removing some edges from the original graph) is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph UMGrph

Theoremumgra0 23283 The empty graph, with vertices but no edges, is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph

Theoremumgra1 23284 The graph with one edge. (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph

Theoremumgraun 23285 If and are graphs, then is a graph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph        UMGrph        UMGrph

Theoremreleupa 23286 The set EulPaths of all Eulerian paths on is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremiseupa 23287* The property " is an Eulerian path on the graph ". An Eulerian path is defined as bijection from the edges to a set a function into the vertices such that for each , is an edge from to . (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)
EulPaths UMGrph

Theoremeupagra 23288 If an eulerian path exists, then is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths UMGrph

Theoremeupai 23289* Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremeupacl 23290 An Eulerian path has length , which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremeupaf1o 23291 The function in an Eulerian path is a bijection from a one-based sequence to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremeupafi 23292 Any graph with an Eulerian path is finite. (Contributed by Mario Carneiro, 7-Apr-2015.)
EulPaths

Theoremeupapf 23293 The function in an Eulerian path is a function from a zero-based finite sequence to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremeupaseg 23294 The -th edge in an eulerian path is the edge from to . (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

Theoremvdgrfval 23295* The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgrval 23296* The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgrf 23297 The vertex degree function on finite graphs is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgr0 23298 The degree of a vertex in an empty graph is zero, because there are no edges. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgrun 23299 The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
UMGrph        UMGrph               VDeg VDeg VDeg

Theoremvdgr1d 23300 The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 <