Home | Metamath
Proof Explorer Theorem List (p. 270 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwlkclwwlklem2 26901* | Lemma 2 for clwlkclwwlk 26903. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
Word ..^ lastS ..^ | ||
Theorem | clwlkclwwlklem3 26902* | Lemma 3 for clwlkclwwlk 26903. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
Word Word ..^ lastS ..^ | ||
Theorem | clwlkclwwlk 26903* | A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.) |
Vtx iEdg USPGraph Word ClWalks lastS substr ClWWalks | ||
Theorem | clwlkclwwlk2 26904* | A closed walk corresponds to a closed walk as word in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.) |
Vtx iEdg USPGraph Word ClWalks ++ ClWWalks | ||
Theorem | clwwlkinwwlk 26905 | If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 23-Jan-2022.) |
WWalksN substr ClWWalksN | ||
Theorem | clwwlksgt0 26906 | There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
ClWWalks | ||
Theorem | clwwlksn0 26907 | There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
ClWWalksN | ||
Theorem | clwwlks1loop 26908 | A closed walk of length 1 is a loop. See also clwlkl1loop 26678. (Contributed by AV, 24-Apr-2021.) |
ClWWalks Edg | ||
Theorem | clwwlksn1loop 26909 | A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.) |
ClWWalksN Edg | ||
Theorem | clwwlksn2 26910 | A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Apr-2021.) |
ClWWalksN Word Vtx Edg | ||
Theorem | clwwlkssswrd 26911 | Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) |
ClWWalks Word Vtx | ||
Theorem | umgrclwwlksge2 26912 | A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
UMGraph ClWWalks | ||
Theorem | clwwlksnfi 26913 | If there is only a finite number of vertices, the number of closed walks of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) |
Vtx ClWWalksN | ||
Theorem | clwwlksel 26914* | Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 25-Apr-2021.) |
WWalksN lastS Word Vtx ..^ Edg lastS Edg ++ | ||
Theorem | clwwlksf 26915* | Lemma 1 for clwwlksbij 26920: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS substr ClWWalksN | ||
Theorem | clwwlksfv 26916* | Lemma 2 for clwwlksbij 26920: the value of function F. (Contributed by Alexander van der Vekens, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS substr substr | ||
Theorem | clwwlksf1 26917* | Lemma 3 for clwwlksbij 26920: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS substr ClWWalksN | ||
Theorem | clwwlksfo 26918* | Lemma 4 for clwwlksbij 26920: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS substr ClWWalksN | ||
Theorem | clwwlksf1o 26919* | Lemma 5 for clwwlksbij 26920: F is a 1-1 onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS substr ClWWalksN | ||
Theorem | clwwlksbij 26920* | There is a bijection between the set of closed walks of a fixed length represented by walks (as word) and the set of closed walks (as words) of a fixed length. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS ClWWalksN | ||
Theorem | clwwlksnwwlkncl 26921* | Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
ClWWalksN ++ WWalksN lastS | ||
Theorem | clwwlksvbij 26922* | There is a bijection between the set of closed walks of a fixed length starting at a fixed vertex represented by walks (as word) and the set of closed walks (as words) of a fixed length starting at a fixed vertex. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
WWalksN lastS ClWWalksN | ||
Theorem | clwwlksext2edg 26923 | If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) |
Vtx Edg Word ++ ClWWalksN lastS | ||
Theorem | wwlksext2clwwlk 26924 | If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) |
Vtx Edg WWalksN lastS ++ ClWWalksN | ||
Theorem | wwlksubclwwlks 26925 | Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 28-Apr-2021.) |
ClWWalksN substr WWalksN | ||
Theorem | clwwisshclwwslemlem 26926* | Lemma for clwwisshclwwslem 26927. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
..^ | ||
Theorem | clwwisshclwwslem 26927* | Lemma for clwwisshclwws 26928. (Contributed by AV, 24-Mar-2018.) (Revised by AV, 28-Apr-2021.) |
Word ..^ ..^ lastS ..^ cyclShift cyclShift cyclShift | ||
Theorem | clwwisshclwws 26928 | Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Mar-2018.) (Revised by AV, 28-Apr-2021.) |
ClWWalks ..^ cyclShift ClWWalks | ||
Theorem | clwwisshclwwsn 26929 | Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jun-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks cyclShift ClWWalks | ||
Theorem | clwwnisshclwwsn 26930 | Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalksN cyclShift ClWWalksN | ||
Theorem | erclwwlksrel 26931 | is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks ClWWalks cyclShift | ||
Theorem | erclwwlkseq 26932* | Two classes are equivalent regarding if both are words and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks ClWWalks cyclShift ClWWalks ClWWalks cyclShift | ||
Theorem | erclwwlkseqlen 26933* | If two classes are equivalent regarding , then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks ClWWalks cyclShift | ||
Theorem | erclwwlksref 26934* | is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks ClWWalks cyclShift ClWWalks | ||
Theorem | erclwwlkssym 26935* | is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 29-Apr-2021.) |
ClWWalks ClWWalks cyclShift | ||
Theorem | erclwwlkstr 26936* | is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalks ClWWalks cyclShift | ||
Theorem | erclwwlks 26937* | is an equivalence relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalks ClWWalks cyclShift ClWWalks | ||
Theorem | eleclclwwlksnlem1 26938* | Lemma 1 for eleclclwwlksn 26953. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift cyclShift cyclShift | ||
Theorem | eleclclwwlksnlem2 26939* | Lemma 2 for eleclclwwlksn 26953. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift cyclShift cyclShift | ||
Theorem | clwwlksnscsh 26940* | The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN ClWWalksN cyclShift Word Vtx cyclShift | ||
Theorem | umgr2cwwk2dif 26941 | If a word represents a closed walk of length at least 2 in a multigraph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
UMGraph ClWWalksN | ||
Theorem | umgr2cwwkdifex 26942* | If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
UMGraph ClWWalksN ..^ | ||
Theorem | erclwwlksnrel 26943 | is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | erclwwlksneq 26944* | Two classes are equivalent regarding if both are words of the same fixed length and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift cyclShift | ||
Theorem | erclwwlksneqlen 26945* | If two classes are equivalent regarding , then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | erclwwlksnref 26946* | is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | erclwwlksnsym 26947* | is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | erclwwlksntr 26948* | is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | erclwwlksn 26949* | is an equivalence relation over the set of closed walks (defined as words) with a fixed length. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift | ||
Theorem | qerclwwlksnfi 26950* | The quotient set of the set of closed walks (defined as words) with a fixed length according to the equivalence relation is finite. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift Vtx | ||
Theorem | hashclwwlksn0 26951* | The number of closed walks (defined as words) with a fixed length is the sum of the sizes of all equivalence classes according to . (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift Vtx | ||
Theorem | eclclwwlksn1 26952* | An equivalence class according to . (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
ClWWalksN cyclShift cyclShift | ||
Theorem | eleclclwwlksn 26953* | A member of an equivalence class according to . (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 1-May-2021.) |
ClWWalksN cyclShift cyclShift | ||
Theorem | hashecclwwlksn1 26954* | The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
ClWWalksN cyclShift | ||
Theorem | umgrhashecclwwlk 26955* | The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number equals this length (in an undirected simple graph). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
ClWWalksN cyclShift UMGraph | ||
Theorem | fusgrhashclwwlkn 26956* | The size of the set of closed walks (defined as words) with a fixed length which is a prime number is the product of the number of equivalence classes for over the set of closed walks and the fixed length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
ClWWalksN cyclShift FinUSGraph | ||
Theorem | clwwlksndivn 26957 | The size of the set of closed walks (defined as words) of length n is divisible by n. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 2-May-2021.) |
FinUSGraph ClWWalksN | ||
Theorem | clwlksfclwwlk2wrd 26958* | The second component of a closed walk is a word over the "vertices". (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr Word Vtx | ||
Theorem | clwlksfclwwlk1hashn 26959* | The size of the first component of a closed walk. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr | ||
Theorem | clwlksfclwwlk1hash 26960* | The size of the first component of a closed walk is an integer in the range between 0 and the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr | ||
Theorem | clwlksfclwwlk2sswd 26961* | The size of a subword of the second component of a closed walk with length of the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr substr | ||
Theorem | clwlksfclwwlk 26962* | There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr FinUSGraph ClWWalksN | ||
Theorem | clwlksfoclwwlk 26963* | There is an onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 2-May-2021.) |
ClWalks substr FinUSGraph ClWWalksN | ||
Theorem | clwlksf1clwwlklem0 26964* | Lemma 1 for clwlksf1clwwlklem 26968. (Contributed by AV, 3-May-2021.) |
ClWalks substr Word iEdg Vtx | ||
Theorem | clwlksf1clwwlklem1 26965* | Lemma 1 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr | ||
Theorem | clwlksf1clwwlklem2 26966* | Lemma 2 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr | ||
Theorem | clwlksf1clwwlklem3 26967* | Lemma 3 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr Word Vtx | ||
Theorem | clwlksf1clwwlklem 26968* | Lemma for clwlksf1clwwlk 26969. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr substr substr | ||
Theorem | clwlksf1clwwlk 26969* | There is a one-to-one function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr FinUSGraph ClWWalksN | ||
Theorem | clwlksf1oclwwlk 26970* | There is a one-to-one onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
ClWalks substr FinUSGraph ClWWalksN | ||
Theorem | clwlkssizeeq 26971* | The size of the set of closed walks (defined as words) of length n corresponds to the size of the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) |
FinUSGraph ClWWalksN ClWalks | ||
Theorem | clwlksndivn 26972* | The size of the set of closed walks of length n is divisible by n. This corresponds to statement 9 in [Huneke] p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p". (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) |
FinUSGraph ClWalks | ||
Theorem | clwwlksndisj 26973* | The sets of closed walks starting at different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) |
Disj ClWWalksN | ||
Theorem | clwwlksnun 26974* | The set of closed walks of fixed length in a simple graph is the union of the closed walks of the fixed length starting at each of the vertices. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) |
Vtx USGraph ClWWalksN ClWWalksN | ||
Theorem | 0ewlk 26975 | The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.) |
NN0* EdgWalks | ||
Theorem | 1ewlk 26976 | A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.) |
NN0* iEdg EdgWalks | ||
Theorem | 0wlk 26977 | A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx Walks | ||
Theorem | is0wlk 26978 | A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Vtx Walks | ||
Theorem | 0wlkonlem1 26979 | Lemma 1 for 0wlkon 26981 and 0trlon 26985. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
Vtx | ||
Theorem | 0wlkonlem2 26980 | Lemma 2 for 0wlkon 26981 and 0trlon 26985. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
Vtx | ||
Theorem | 0wlkon 26981 | A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Vtx WalksOn | ||
Theorem | 0wlkons1 26982 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
Vtx WalksOn | ||
Theorem | 0trl 26983 | A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx Trails | ||
Theorem | is0trl 26984 | A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Vtx Trails | ||
Theorem | 0trlon 26985 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Vtx TrailsOn | ||
Theorem | 0pth 26986 | A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx Paths | ||
Theorem | 0spth 26987 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx SPaths | ||
Theorem | 0pthon 26988 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx PathsOn | ||
Theorem | 0pthon1 26989 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) |
Vtx PathsOn | ||
Theorem | 0pthonv 26990* | For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.) |
Vtx PathsOn | ||
Theorem | 0clwlk 26991 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
Vtx ClWalks | ||
Theorem | 0clwlk0 26992 | There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
ClWalks | ||
Theorem | 0crct 26993 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Circuits Vtx | ||
Theorem | 0cycl 26994 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Cycles Vtx | ||
Theorem | 1pthdlem1 26995 | Lemma 1 for 1pthd 27003. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
..^ | ||
Theorem | 1pthdlem2 26996 | Lemma 2 for 1pthd 27003. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
..^ | ||
Theorem | 1wlkdlem1 26997 | Lemma 1 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
Theorem | 1wlkdlem2 26998 | Lemma 2 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
Theorem | 1wlkdlem3 26999 | Lemma 3 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
Word | ||
Theorem | 1wlkdlem4 27000* | Lemma 4 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
..^if- |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |