Home | Metamath
Proof Explorer Theorem List (p. 288 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rusgrnumwwlklem 28701* | Lemma for rusgrnumwwlk 28706 etc. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((π β π β§ π β β0) β (ππΏπ) = (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) | ||
Theorem | rusgrnumwwlkb0 28702* | Induction base 0 for rusgrnumwwlk 28706. Here, we do not need the regularity of the graph yet. (Contributed by Alexander van der Vekens, 24-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ β USPGraph β§ π β π) β (ππΏ0) = 1) | ||
Theorem | rusgrnumwwlkb1 28703* | Induction base 1 for rusgrnumwwlk 28706. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph πΎ β§ π β π) β (ππΏ1) = πΎ) | ||
Theorem | rusgr0edg 28704* | Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph 0 β§ π β π β§ π β β) β (ππΏπ) = 0) | ||
Theorem | rusgrnumwwlks 28705* | Induction step for rusgrnumwwlk 28706. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) (Proof shortened by AV, 27-May-2022.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β ((ππΏπ) = (πΎβπ) β (ππΏ(π + 1)) = (πΎβ(π + 1)))) | ||
Theorem | rusgrnumwwlk 28706* |
In a πΎ-regular graph, the number of walks
of a fixed length π
from a fixed vertex is πΎ to the power of π. By
definition,
(π
WWalksN πΊ) is the
set of walks (as words) with length π,
and (ππΏπ) is the number of walks with length
π
starting at
the vertex π. Because of the πΎ-regularity, a walk can be
continued in πΎ different ways at the end vertex of
the walk, and
this repeated π times.
This theorem even holds for π = 0: in this case, the walk consists of only one vertex π, so the number of walks of length π = 0 starting with π is (πΎβ0) = 1. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (ππΏπ) = (πΎβπ)) | ||
Theorem | rusgrnumwwlkg 28707* | In a πΎ-regular graph, the number of walks (as words) of a fixed length π from a fixed vertex is πΎ to the power of π. Closed form of rusgrnumwwlk 28706. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) | ||
Theorem | rusgrnumwlkg 28708* | In a k-regular graph, the number of walks of a fixed length n from a fixed vertex is k to the power of n. This theorem corresponds to statement 11 in [Huneke] p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular." This theorem even holds for n=0: then the walk consists of only one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) (Proof shortened by AV, 5-Aug-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (β―β{π€ β (WalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)}) = (πΎβπ)) | ||
Theorem | clwwlknclwwlkdif 28709* | The set π΄ of walks of length π starting with a fixed vertex π and ending not at this vertex is the difference between the set πΆ of walks of length π starting with this vertex π and the set π΅ of closed walks of length π anchored at this vertex π. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) (Revised by AV, 16-Mar-2022.) |
β’ π΄ = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)} & β’ π΅ = (π(π WWalksNOn πΊ)π) & β’ πΆ = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β β’ π΄ = (πΆ β π΅) | ||
Theorem | clwwlknclwwlkdifnum 28710* | In a πΎ-regular graph, the size of the set π΄ of walks of length π starting with a fixed vertex π and ending not at this vertex is the difference between πΎ to the power of π and the size of the set π΅ of closed walks of length π anchored at this vertex π. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) (Revised by AV, 8-Mar-2022.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π΄ = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)} & β’ π΅ = (π(π WWalksNOn πΊ)π) & β’ π = (VtxβπΊ) β β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β (β―βπ΄) = ((πΎβπ) β (β―βπ΅))) | ||
In general, a closed walk is an alternating sequence of vertices and edges, as defined in df-clwlks 28505: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n), with p(n) = p(0). Often, it is sufficient to refer to a walk by the (cyclic) sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(0), see the corresponding remark on cycles (which are special closed walks) in [Diestel] p. 7. As for "walks as words" in general, the concept of a Word, see df-word 14331, is also used in Definitions df-clwwlk 28712 and df-clwwlkn 28755, and the representation of a closed walk as the sequence of its vertices is called "closed walk as word". In contrast to "walks as words", the terminating vertex p(n) of a closed walk is omitted in the representation of a closed walk as word, see definitions df-clwwlk 28712, df-clwwlkn 28755 and df-clwwlknon 28818, because it is always equal to the first vertex of the closed walk. This represenation has the advantage that the vertices can be cyclically shifted without changing the represented closed walk. Furthermore, the length of a closed walk (i.e. the number of its edges) equals the number of symbols/vertices of the word representing the closed walk. To avoid to handle the degenerate case of representing a (closed) walk of length 0 by the empty word, this case is excluded within the definition (π€ β β ). This is because a walk of length 0 is anchored at an arbitrary vertex by the general definition for closed walks, see 0clwlkv 28861, which neither can be reflected by the empty word nor by a singleton word β¨βπ£ββ© with vertex v : β¨βπ£ββ© represents the walk "π£π£", which is a (closed) walk of length 1 (if there is an edge/loop from π£ to π£), see loopclwwlkn1b 28772. Therefore, a closed walk corresponds to a closed walk as word only for walks of length at least 1, see clwlkclwwlk2 28733 or clwlkclwwlken 28742. Although the set ClWWalksN of all closed walks of a fixed length as words over the set of vertices is defined as function over β0, the fixed length is usually not 0, because (0 ClWWalksN πΊ) = β (see clwwlkn0 28758). Analogous to (π΄(π WWalksNOn πΊ)π΅), the set of walks of a fixed length π between two vertices π΄ and π΅, the set (π(ClWWalksNOnβπΊ)π) of closed walks of a fixed length π anchored at a fixed vertex π is defined by df-clwwlknon 28818. This definition is also based on β0 instead of β, with (π(ClWWalksNOnβπΊ)0) = β (see clwwlk0on0 28822). clwwlknon1le1 28831 states that there is at most one (closed) walk of length 1 on a vertex, which would consist of a loop (see clwwlknon1loop 28828). And in a πΎ-regular graph, there are πΎ closed walks of length 2 on each vertex, see clwwlknon2num 28835. | ||
Syntax | cclwwlk 28711 | Extend class notation with closed walks (in an undirected graph) as word over the set of vertices. |
class ClWWalks | ||
Definition | df-clwwlk 28712* | Define the set of all closed walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 28505. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
β’ ClWWalks = (π β V β¦ {π€ β Word (Vtxβπ) β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β§ {(lastSβπ€), (π€β0)} β (Edgβπ))}) | ||
Theorem | clwwlk 28713* | The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (ClWWalksβπΊ) = {π€ β Word π β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} | ||
Theorem | isclwwlk 28714* | Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (ClWWalksβπΊ) β ((π β Word π β§ π β β ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) | ||
Theorem | clwwlkbp 28715 | Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (ClWWalksβπΊ) β (πΊ β V β§ π β Word π β§ π β β )) | ||
Theorem | clwwlkgt0 28716 | 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βπΊ) β 0 < (β―βπ)) | ||
Theorem | clwwlksswrd 28717 | 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 | clwwlk1loop 28718 | A closed walk of length 1 is a loop. See also clwlkl1loop 28517. (Contributed by AV, 24-Apr-2021.) |
β’ ((π β (ClWWalksβπΊ) β§ (β―βπ) = 1) β {(πβ0), (πβ0)} β (EdgβπΊ)) | ||
Theorem | clwwlkccatlem 28719* | Lemma for clwwlkccat 28720: index π is shifted up by (β―βπ΄), and the case π = ((β―βπ΄) β 1) is covered by the "bridge" {(lastSβπ΄), (π΅β0)} = {(lastSβπ΄), (π΄β0)} β (EdgβπΊ). (Contributed by AV, 23-Apr-2022.) |
β’ ((((π΄ β Word (VtxβπΊ) β§ π΄ β β ) β§ βπ β (0..^((β―βπ΄) β 1)){(π΄βπ), (π΄β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ΄), (π΄β0)} β (EdgβπΊ)) β§ ((π΅ β Word (VtxβπΊ) β§ π΅ β β ) β§ βπ β (0..^((β―βπ΅) β 1)){(π΅βπ), (π΅β(π + 1))} β (EdgβπΊ) β§ {(lastSβπ΅), (π΅β0)} β (EdgβπΊ)) β§ (π΄β0) = (π΅β0)) β βπ β (0..^((β―β(π΄ ++ π΅)) β 1)){((π΄ ++ π΅)βπ), ((π΄ ++ π΅)β(π + 1))} β (EdgβπΊ)) | ||
Theorem | clwwlkccat 28720 | The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022.) |
β’ ((π΄ β (ClWWalksβπΊ) β§ π΅ β (ClWWalksβπΊ) β§ (π΄β0) = (π΅β0)) β (π΄ ++ π΅) β (ClWWalksβπΊ)) | ||
Theorem | umgrclwwlkge2 28721 | 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βπΊ) β 2 β€ (β―βπ))) | ||
Theorem | clwlkclwwlklem2a1 28722* | Lemma 1 for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 21-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ)) | ||
Theorem | clwlkclwwlklem2a2 28723* | Lemma 2 for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) | ||
Theorem | clwlkclwwlklem2a3 28724* | Lemma 3 for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((π β Word π β§ 2 β€ (β―βπ)) β (πβ(β―βπΉ)) = (lastSβπ)) | ||
Theorem | clwlkclwwlklem2fv1 28725* | Lemma 4a for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ (((β―βπ) β β0 β§ πΌ β (0..^((β―βπ) β 2))) β (πΉβπΌ) = (β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) | ||
Theorem | clwlkclwwlklem2fv2 28726* | Lemma 4b for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ (((β―βπ) β β0 β§ 2 β€ (β―βπ)) β (πΉβ((β―βπ) β 2)) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) | ||
Theorem | clwlkclwwlklem2a4 28727* | Lemma 4 for clwlkclwwlklem2a 28728. (Contributed by Alexander van der Vekens, 21-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((πΈ:dom πΈβ1-1βπ β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ πΌ β (0..^((β―βπ) β 1))) β ({(πβπΌ), (πβ(πΌ + 1))} β ran πΈ β (πΈβ(πΉβπΌ)) = {(πβπΌ), (πβ(πΌ + 1))}))) | ||
Theorem | clwlkclwwlklem2a 28728* | Lemma for clwlkclwwlklem2 28730. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((πΈ:dom πΈβ1-1βπ β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((πΉ β Word dom πΈ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπΉ))))) | ||
Theorem | clwlkclwwlklem1 28729* | Lemma 1 for clwlkclwwlk 28732. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ ((πΈ:dom πΈβ1-1βπ β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) | ||
Theorem | clwlkclwwlklem2 28730* | Lemma 2 for clwlkclwwlk 28732. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ (((πΈ:dom πΈβ1-1βπ β§ πΉ β Word dom πΈ) β§ (π:(0...(β―βπΉ))βΆπ β§ 2 β€ (β―βπ)) β§ (βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπΉ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπΉ) β 1)), (πβ0)} β ran πΈ)) | ||
Theorem | clwlkclwwlklem3 28731* | Lemma 3 for clwlkclwwlk 28732. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
β’ ((πΈ:dom πΈβ1-1βπ β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) | ||
Theorem | clwlkclwwlk 28732* | 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.) (Revised by AV, 30-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ π(ClWalksβπΊ)π β ((lastSβπ) = (πβ0) β§ (π prefix ((β―βπ) β 1)) β (ClWWalksβπΊ)))) | ||
Theorem | clwlkclwwlk2 28733* | 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.) (Proof shortened by AV, 2-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ π(ClWalksβπΊ)(π ++ β¨β(πβ0)ββ©) β π β (ClWWalksβπΊ))) | ||
Theorem | clwlkclwwlkflem 28734* | Lemma for clwlkclwwlkf 28738. (Contributed by AV, 24-May-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) β β’ (π β πΆ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) | ||
Theorem | clwlkclwwlkf1lem2 28735* | Lemma 2 for clwlkclwwlkf1 28740. (Contributed by AV, 24-May-2022.) (Revised by AV, 30-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) & β’ π· = (1st βπ) & β’ πΈ = (2nd βπ) β β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) | ||
Theorem | clwlkclwwlkf1lem3 28736* | Lemma 3 for clwlkclwwlkf1 28740. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 30-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) & β’ π· = (1st βπ) & β’ πΈ = (2nd βπ) β β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β βπ β (0...(β―βπ΄))(π΅βπ) = (πΈβπ)) | ||
Theorem | clwlkclwwlkfolem 28737* | Lemma for clwlkclwwlkfo 28739. (Contributed by AV, 25-May-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} β β’ ((π β Word (VtxβπΊ) β§ 1 β€ (β―βπ) β§ β¨π, (π ++ β¨β(πβ0)ββ©)β© β (ClWalksβπΊ)) β β¨π, (π ++ β¨β(πβ0)ββ©)β© β πΆ) | ||
Theorem | clwlkclwwlkf 28738* | πΉ is a function from the nonempty closed walks into the closed walks as word in a simple pseudograph. (Contributed by AV, 23-May-2022.) (Revised by AV, 29-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ πΉ = (π β πΆ β¦ ((2nd βπ) prefix ((β―β(2nd βπ)) β 1))) β β’ (πΊ β USPGraph β πΉ:πΆβΆ(ClWWalksβπΊ)) | ||
Theorem | clwlkclwwlkfo 28739* | πΉ is a function from the nonempty closed walks onto the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by AV, 29-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ πΉ = (π β πΆ β¦ ((2nd βπ) prefix ((β―β(2nd βπ)) β 1))) β β’ (πΊ β USPGraph β πΉ:πΆβontoβ(ClWWalksβπΊ)) | ||
Theorem | clwlkclwwlkf1 28740* | πΉ is a one-to-one function from the nonempty closed walks into the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 29-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ πΉ = (π β πΆ β¦ ((2nd βπ) prefix ((β―β(2nd βπ)) β 1))) β β’ (πΊ β USPGraph β πΉ:πΆβ1-1β(ClWWalksβπΊ)) | ||
Theorem | clwlkclwwlkf1o 28741* | πΉ is a bijection between the nonempty closed walks and the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 29-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ πΉ = (π β πΆ β¦ ((2nd βπ) prefix ((β―β(2nd βπ)) β 1))) β β’ (πΊ β USPGraph β πΉ:πΆβ1-1-ontoβ(ClWWalksβπΊ)) | ||
Theorem | clwlkclwwlken 28742* | The set of the nonempty closed walks and the set of closed walks as word are equinumerous in a simple pseudograph. (Contributed by AV, 25-May-2022.) (Proof shortened by AV, 4-Nov-2022.) |
β’ (πΊ β USPGraph β {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} β (ClWWalksβπΊ)) | ||
Theorem | clwwisshclwwslemlem 28743* | Lemma for clwwisshclwwslem 28744. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
β’ (((πΏ β (β€β₯β2) β§ π΄ β β€ β§ π΅ β β€) β§ βπ β (0..^(πΏ β 1)){(πβπ), (πβ(π + 1))} β π β§ {(πβ(πΏ β 1)), (πβ0)} β π ) β {(πβ((π΄ + π΅) mod πΏ)), (πβ(((π΄ + 1) + π΅) mod πΏ))} β π ) | ||
Theorem | clwwisshclwwslem 28744* | Lemma for clwwisshclwws 28745. (Contributed by AV, 24-Mar-2018.) (Revised by AV, 28-Apr-2021.) |
β’ ((π β Word π β§ π β (1..^(β―βπ))) β ((βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β βπ β (0..^((β―β(π cyclShift π)) β 1)){((π cyclShift π)βπ), ((π cyclShift π)β(π + 1))} β πΈ)) | ||
Theorem | clwwisshclwws 28745 | 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βπΊ) β§ π β (0..^(β―βπ))) β (π cyclShift π) β (ClWWalksβπΊ)) | ||
Theorem | clwwisshclwwsn 28746 | 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βπΊ) β§ π β (0...(β―βπ))) β (π cyclShift π) β (ClWWalksβπΊ)) | ||
Theorem | erclwwlkrel 28747 | βΌ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
β’ βΌ = {β¨π’, π€β© β£ (π’ β (ClWWalksβπΊ) β§ π€ β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ Rel βΌ | ||
Theorem | erclwwlkeq 28748* | 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ ((π β π β§ π β π) β (π βΌ π β (π β (ClWWalksβπΊ) β§ π β (ClWWalksβπΊ) β§ βπ β (0...(β―βπ))π = (π cyclShift π)))) | ||
Theorem | erclwwlkeqlen 28749* | 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ ((π β π β§ π β π) β (π βΌ π β (β―βπ) = (β―βπ))) | ||
Theorem | erclwwlkref 28750* | βΌ 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ (π₯ β (ClWWalksβπΊ) β π₯ βΌ π₯) | ||
Theorem | erclwwlksym 28751* | βΌ 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ (π₯ βΌ π¦ β π¦ βΌ π₯) | ||
Theorem | erclwwlktr 28752* | βΌ 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ ((π₯ βΌ π¦ β§ π¦ βΌ π§) β π₯ βΌ π§) | ||
Theorem | erclwwlk 28753* | βΌ 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βπΊ) β§ βπ β (0...(β―βπ€))π’ = (π€ cyclShift π))} β β’ βΌ Er (ClWWalksβπΊ) | ||
Syntax | cclwwlkn 28754 | Extend class notation with closed walks (in an undirected graph) of a fixed length as word over the set of vertices. |
class ClWWalksN | ||
Definition | df-clwwlkn 28755* | Define the set of all closed walks of a fixed length π as words over the set of vertices in a graph π. If 0 < π, such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 28505. For π = 0, the set is empty, see clwwlkn0 28758. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.) |
β’ ClWWalksN = (π β β0, π β V β¦ {π€ β (ClWWalksβπ) β£ (β―βπ€) = π}) | ||
Theorem | clwwlkn 28756* | The set of closed walks of a fixed length π as words over the set of vertices in a graph πΊ. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.) |
β’ (π ClWWalksN πΊ) = {π€ β (ClWWalksβπΊ) β£ (β―βπ€) = π} | ||
Theorem | isclwwlkn 28757 | A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π)) | ||
Theorem | clwwlkn0 28758 | 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.) |
β’ (0 ClWWalksN πΊ) = β | ||
Theorem | clwwlkneq0 28759 | Sufficient conditions for ClWWalksN to be empty. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 24-Feb-2022.) |
β’ ((πΊ β V β¨ π β β) β (π ClWWalksN πΊ) = β ) | ||
Theorem | clwwlkclwwlkn 28760 | A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β π β (ClWWalksβπΊ)) | ||
Theorem | clwwlksclwwlkn 28761 | The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (π ClWWalksN πΊ) β (ClWWalksβπΊ) | ||
Theorem | clwwlknlen 28762 | The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β (β―βπ) = π) | ||
Theorem | clwwlknnn 28763 | The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β π β β) | ||
Theorem | clwwlknwrd 28764 | A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (π ClWWalksN πΊ) β π β Word π) | ||
Theorem | clwwlknbp 28765 | Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π ClWWalksN πΊ) β (π β Word π β§ (β―βπ) = π)) | ||
Theorem | isclwwlknx 28766* | Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β β β (π β (π ClWWalksN πΊ) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π))) | ||
Theorem | clwwlknp 28767* | Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (π ClWWalksN πΊ) β ((π β Word π β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) | ||
Theorem | clwwlknwwlksn 28768 | A word representing a closed walk of length π also represents a walk of length π β 1. The walk is one edge shorter than the closed walk, because the last edge connecting the last with the first vertex is missing. For example, if β¨βπππββ© β (3 ClWWalksN πΊ) represents a closed walk "abca" of length 3, then β¨βπππββ© β (2 WWalksN πΊ) represents a walk "abc" (not closed if π β π) of length 2, and β¨βππππββ© β (3 WWalksN πΊ) represents also a closed walk "abca" of length 3. (Contributed by AV, 24-Jan-2022.) (Revised by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β π β ((π β 1) WWalksN πΊ)) | ||
Theorem | clwwlknlbonbgr1 28769 | The last but one vertex in a closed walk is a neighbor of the first vertex of the closed walk. (Contributed by AV, 17-Feb-2022.) |
β’ ((πΊ β USGraph β§ π β (π ClWWalksN πΊ)) β (πβ(π β 1)) β (πΊ NeighbVtx (πβ0))) | ||
Theorem | clwwlkinwwlk 28770 | 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.) (Revised by AV, 30-Oct-2022.) |
β’ (((π β β β§ π β (β€β₯βπ)) β§ π β (π WWalksN πΊ) β§ (πβπ) = (πβ0)) β (π prefix π) β (π ClWWalksN πΊ)) | ||
Theorem | clwwlkn1 28771 | A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021.) (Revised by AV, 11-Feb-2022.) |
β’ (π β (1 ClWWalksN πΊ) β ((β―βπ) = 1 β§ π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ))) | ||
Theorem | loopclwwlkn1b 28772 | The singleton word consisting of a vertex π represents a closed walk of length 1 iff there is a loop at vertex π. (Contributed by AV, 11-Feb-2022.) |
β’ (π β (VtxβπΊ) β ({π} β (EdgβπΊ) β β¨βπββ© β (1 ClWWalksN πΊ))) | ||
Theorem | clwwlkn1loopb 28773* | A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022.) |
β’ (π β (1 ClWWalksN πΊ) β βπ£ β (VtxβπΊ)(π = β¨βπ£ββ© β§ {π£} β (EdgβπΊ))) | ||
Theorem | clwwlkn2 28774 | 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.) |
β’ (π β (2 ClWWalksN πΊ) β ((β―βπ) = 2 β§ π β Word (VtxβπΊ) β§ {(πβ0), (πβ1)} β (EdgβπΊ))) | ||
Theorem | clwwlknfi 28775 | 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.) (Proof shortened by AV, 22-Mar-2022.) (Proof shortened by JJ, 18-Nov-2022.) |
β’ ((VtxβπΊ) β Fin β (π ClWWalksN πΊ) β Fin) | ||
Theorem | clwwlkel 28776* | 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βπ€) = (π€β0)} β β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β π·) | ||
Theorem | clwwlkf 28777* | Lemma 1 for clwwlkf1o 28781: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} & β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) β β’ (π β β β πΉ:π·βΆ(π ClWWalksN πΊ)) | ||
Theorem | clwwlkfv 28778* | Lemma 2 for clwwlkf1o 28781: the value of function πΉ. (Contributed by Alexander van der Vekens, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} & β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) β β’ (π β π· β (πΉβπ) = (π prefix π)) | ||
Theorem | clwwlkf1 28779* | Lemma 3 for clwwlkf1o 28781: πΉ is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} & β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) β β’ (π β β β πΉ:π·β1-1β(π ClWWalksN πΊ)) | ||
Theorem | clwwlkfo 28780* | Lemma 4 for clwwlkf1o 28781: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} & β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) β β’ (π β β β πΉ:π·βontoβ(π ClWWalksN πΊ)) | ||
Theorem | clwwlkf1o 28781* | F is a 1-1 onto function, that means that there is a bijection between the set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the 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.) (Revised by AV, 1-Nov-2022.) |
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} & β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) β β’ (π β β β πΉ:π·β1-1-ontoβ(π ClWWalksN πΊ)) | ||
Theorem | clwwlken 28782* | The set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length are equinumerous. (Contributed by AV, 5-Jun-2022.) (Proof shortened by AV, 2-Nov-2022.) |
β’ (π β β β {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} β (π ClWWalksN πΊ)) | ||
Theorem | clwwlknwwlkncl 28783* | 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.) (Revised by AV, 22-Mar-2022.) |
β’ (π β (π ClWWalksN πΊ) β (π ++ β¨β(πβ0)ββ©) β {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)}) | ||
Theorem | clwwlkwwlksb 28784 | A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Word π β§ π β β ) β (π β (ClWWalksβπΊ) β (π ++ β¨β(πβ0)ββ©) β (WWalksβπΊ))) | ||
Theorem | clwwlknwwlksnb 28785 | A word over vertices represents a closed walk of a fixed length π greater than zero iff the word concatenated with its first symbol represents a walk of length π. This theorem would not hold for π = 0 and π = β , because (π ++ β¨β(πβ0)ββ©) = β¨ββ ββ© β (0 WWalksN πΊ) could be true, but not π β (0 ClWWalksN πΊ) β β β β . (Contributed by AV, 4-Mar-2022.) (Proof shortened by AV, 22-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Word π β§ π β β) β (π β (π ClWWalksN πΊ) β (π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ))) | ||
Theorem | clwwlkext2edg 28786 | 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.) (Proof shortened by AV, 22-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((π β Word π β§ π β π β§ π β (β€β₯β2)) β§ (π ++ β¨βπββ©) β (π ClWWalksN πΊ)) β ({(lastSβπ), π} β πΈ β§ {π, (πβ0)} β πΈ)) | ||
Theorem | wwlksext2clwwlk 28787 | 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.) (Revised by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π β (π WWalksN πΊ) β§ π β π) β (({(lastSβπ), π} β πΈ β§ {π, (πβ0)} β πΈ) β (π ++ β¨βπββ©) β ((π + 2) ClWWalksN πΊ))) | ||
Theorem | wwlksubclwwlk 28788 | 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.) (Revised by AV, 1-Nov-2022.) |
β’ ((π β β β§ π β (β€β₯β(π + 1))) β (π β (π ClWWalksN πΊ) β (π prefix π) β ((π β 1) WWalksN πΊ))) | ||
Theorem | clwwnisshclwwsn 28789 | 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.) (Proof shortened by AV, 22-Mar-2022.) |
β’ ((π β (π ClWWalksN πΊ) β§ π β (0...π)) β (π cyclShift π) β (π ClWWalksN πΊ)) | ||
Theorem | eleclclwwlknlem1 28790* | Lemma 1 for eleclclwwlkn 28806. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
β’ π = (π ClWWalksN πΊ) β β’ ((πΎ β (0...π) β§ (π β π β§ π β π)) β ((π = (π cyclShift πΎ) β§ βπ β (0...π)π = (π cyclShift π)) β βπ β (0...π)π = (π cyclShift π))) | ||
Theorem | eleclclwwlknlem2 28791* | Lemma 2 for eleclclwwlkn 28806. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
β’ π = (π ClWWalksN πΊ) β β’ (((π β (0...π) β§ π = (π₯ cyclShift π)) β§ (π β π β§ π₯ β π)) β (βπ β (0...π)π = (π₯ cyclShift π) β βπ β (0...π)π = (π cyclShift π))) | ||
Theorem | clwwlknscsh 28792* | 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.) |
β’ ((π β β0 β§ π β (π ClWWalksN πΊ)) β {π¦ β (π ClWWalksN πΊ) β£ βπ β (0...π)π¦ = (π cyclShift π)} = {π¦ β Word (VtxβπΊ) β£ βπ β (0...π)π¦ = (π cyclShift π)}) | ||
Theorem | clwwlknccat 28793 | The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk with a length which is the sum of the lengths of the two walks. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 24-Apr-2022.) |
β’ ((π΄ β (π ClWWalksN πΊ) β§ π΅ β (π ClWWalksN πΊ) β§ (π΄β0) = (π΅β0)) β (π΄ ++ π΅) β ((π + π) ClWWalksN πΊ)) | ||
Theorem | umgr2cwwk2dif 28794 | 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 β§ π β (β€β₯β2) β§ π β (π ClWWalksN πΊ)) β (πβ1) β (πβ0)) | ||
Theorem | umgr2cwwkdifex 28795* | 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 β§ π β (β€β₯β2) β§ π β (π ClWWalksN πΊ)) β βπ β (0..^π)(πβπ) β (πβ0)) | ||
Theorem | erclwwlknrel 28796 | βΌ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
β’ π = (π ClWWalksN πΊ) & β’ βΌ = {β¨π‘, π’β© β£ (π‘ β π β§ π’ β π β§ βπ β (0...π)π‘ = (π’ cyclShift π))} β β’ Rel βΌ | ||
Theorem | erclwwlkneq 28797* | 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 πΊ) & β’ βΌ = {β¨π‘, π’β© β£ (π‘ β π β§ π’ β π β§ βπ β (0...π)π‘ = (π’ cyclShift π))} β β’ ((π β π β§ π β π) β (π βΌ π β (π β π β§ π β π β§ βπ β (0...π)π = (π cyclShift π)))) | ||
Theorem | erclwwlkneqlen 28798* | 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 πΊ) & β’ βΌ = {β¨π‘, π’β© β£ (π‘ β π β§ π’ β π β§ βπ β (0...π)π‘ = (π’ cyclShift π))} β β’ ((π β π β§ π β π) β (π βΌ π β (β―βπ) = (β―βπ))) | ||
Theorem | erclwwlknref 28799* | βΌ 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.) (Proof shortened by AV, 23-Mar-2022.) |
β’ π = (π ClWWalksN πΊ) & β’ βΌ = {β¨π‘, π’β© β£ (π‘ β π β§ π’ β π β§ βπ β (0...π)π‘ = (π’ cyclShift π))} β β’ (π₯ β π β π₯ βΌ π₯) | ||
Theorem | erclwwlknsym 28800* | βΌ 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 πΊ) & β’ βΌ = {β¨π‘, π’β© β£ (π‘ β π β§ π’ β π β§ βπ β (0...π)π‘ = (π’ cyclShift π))} β β’ (π₯ βΌ π¦ β π¦ βΌ π₯) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |