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

 Color key: Metamath Proof Explorer (1-21811) Hilbert Space Explorer (21812-23334) Users' Mathboxes (23335-32225)

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

Theoremcvmsss 24401* 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 24402* An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

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

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

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

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

Theoremcvmscld 24407* 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 24408* An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
t t        CovMap

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

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

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

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

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

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

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

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

Theoremcvmliftmoi 24417 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 24418* 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 24419* Lemma for cvmlift 24433. In cvmliftlem15 24432, 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 24420* Lemma for cvmlift 24433. is a subset of for each . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

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

Theoremcvmliftlem4 24422* Lemma for cvmlift 24433. 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 24423* Lemma for cvmlift 24433. 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 24424* Lemma for cvmlift 24433. Induction step for cvmliftlem7 24425. 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 24425* Lemma for cvmlift 24433. Prove by induction that every function is well-defined (we can immediately follow this theorem with cvmliftlem6 24424 to show functionality and lifting of ). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem8 24426* Lemma for cvmlift 24433. 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 24427* Lemma for cvmlift 24433. 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 24428* Lemma for cvmlift 24433. 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 24424, cvmliftlem7 24425 (to show it is a function and a lift), cvmliftlem8 24426 (to show it is continuous), and cvmliftlem9 24427 (to show that different functions agree on the intersection of their domains, so that the pasting lemma paste 17239 gives that is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap                                                                       t        t

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

Theoremcvmliftlem13 24430* Lemma for cvmlift 24433. 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 24431* Lemma for cvmlift 24433. Putting the results of cvmliftlem11 24429, cvmliftlem13 24430 and cvmliftmo 24418 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 24432* Lemma for cvmlift 24433. Discharge the assumptions of cvmliftlem14 24431. 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 18679, 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 7248 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 24431. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmlift 24433* 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 24419 thru cvmliftlem15 24432. (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

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

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

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

Theoremcvmlift2lem9a 24437* Lemma for cvmlift2 24450 and cvmlift3 24462. (Contributed by Mario Carneiro, 9-Jul-2015.)
t t        CovMap                                                                t

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcvmlift2 24450* A two-dimensional version of cvmlift 24433. 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 24451* Lemma for cvmliftpht 24452. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

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

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

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

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

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

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

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

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

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

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

Theoremcvmlift3 24462* A general version of cvmlift 24433. 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

19.4.10  Undirected multigraphs

Note: The definition df-umgra 21026 of undirected multigraphs and the corresponding theorems are already moved to the main part of set.mm. The remaining definitions and theorems of this section will be moved soon.

Syntaxceup 24463 Extend class notation with Eulerian paths.
EulPaths

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

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

Definitiondf-vdgr 24466* 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

Theoremreleupa 24467 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 24468* 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 24469 If an eulerian path exists, then is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths UMGrph

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

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

Theoremeupaf1o 24472 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 24473 Any graph with an Eulerian path is finite. (Contributed by Mario Carneiro, 7-Apr-2015.)
EulPaths

Theoremeupapf 24474 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 24475 The -th edge in an eulerian path is the edge from to . (Contributed by Mario Carneiro, 12-Mar-2015.)
EulPaths

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

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

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

Theoremvdgr0 24479 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 24480 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 24481 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

Theoremvdgr1b 24482 The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgr1c 24483 The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremvdgr1a 24484 The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremeupa0 24485 There is an Eulerian path on the empty graph. (Contributed by Mario Carneiro, 7-Apr-2015.)
EulPaths

Theoremeupares 24486 The restriction of an Eulerian path to an initial segment of the path forms an Eulerian path on the subgraph consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)
EulPaths                                    EulPaths

Theoremeupap1 24487 Append one path segment to an Eulerian path (enlarging the graph to add the new edge). (Contributed by Mario Carneiro, 7-Apr-2015.)
EulPaths                                    EulPaths

Theoremeupath2lem1 24488 Lemma for eupath2 24491. (Contributed by Mario Carneiro, 8-Apr-2015.)

Theoremeupath2lem2 24489 Lemma for eupath2 24491. (Contributed by Mario Carneiro, 8-Apr-2015.)

Theoremeupath2lem3 24490* Lemma for eupath2 24491. (Contributed by Mario Carneiro, 8-Apr-2015.)
EulPaths                             VDeg        VDeg

Theoremeupath2 24491* The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.)
EulPaths        VDeg

Theoremeupath 24492* A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.)
EulPaths VDeg

Theoremvdeg0i 24493 The base case for the induction for calculating the degree of a vertex. The degree of in the empty graph is . (Contributed by Mario Carneiro, 12-Mar-2015.)
VDeg

Theoremumgrabi 24494* Show that an unordered pair is a valid edge in a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)

Theoremvdegp1ai 24495* The induction step for a vertex degree calculation. If the degree of in the edge set is , then adding to the edge set, where , yields degree as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Word               VDeg                                    concat        VDeg

Theoremvdegp1bi 24496* The induction step for a vertex degree calculation. If the degree of in the edge set is , then adding to the edge set, where , yields degree . (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Word