![]() |
Metamath
Proof Explorer Theorem List (p. 295 of 480) | < 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wlklnwwlkln2 29401* | A walk of length π as word corresponds to the sequence of vertices in a walk of length π in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (πΊ β USPGraph β (π β (π WWalksN πΊ) β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) | ||
Theorem | wlklnwwlkn 29402* | A walk of length π as word corresponds to a walk with length π in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (πΊ β USPGraph β (βπ(π(WalksβπΊ)π β§ (β―βπ) = π) β π β (π WWalksN πΊ))) | ||
Theorem | wlklnwwlklnupgr2 29403* | A walk of length π as word corresponds to the sequence of vertices in a walk of length π in a pseudograph. This variant of wlklnwwlkln2 29401 does not require πΊ to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (πΊ β UPGraph β (π β (π WWalksN πΊ) β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) | ||
Theorem | wlklnwwlknupgr 29404* | A walk of length π as word corresponds to a walk with length π in a pseudograph. This variant of wlkiswwlks 29394 does not require πΊ to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (πΊ β UPGraph β (βπ(π(WalksβπΊ)π β§ (β―βπ) = π) β π β (π WWalksN πΊ))) | ||
Theorem | wlknewwlksn 29405 | If a walk in a pseudograph has length π, then the sequence of the vertices of the walk is a word representing the walk as word of length π. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 11-Apr-2021.) |
β’ (((πΊ β UPGraph β§ π β (WalksβπΊ)) β§ (π β β0 β§ (β―β(1st βπ)) = π)) β (2nd βπ) β (π WWalksN πΊ)) | ||
Theorem | wlknwwlksnbij 29406* | The mapping (π‘ β π β¦ (2nd βπ‘)) is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.) |
β’ π = {π β (WalksβπΊ) β£ (β―β(1st βπ)) = π} & β’ π = (π WWalksN πΊ) & β’ πΉ = (π‘ β π β¦ (2nd βπ‘)) β β’ ((πΊ β USPGraph β§ π β β0) β πΉ:πβ1-1-ontoβπ) | ||
Theorem | wlknwwlksnen 29407* | In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 5-Aug-2022.) |
β’ ((πΊ β USPGraph β§ π β β0) β {π β (WalksβπΊ) β£ (β―β(1st βπ)) = π} β (π WWalksN πΊ)) | ||
Theorem | wlknwwlksneqs 29408* | The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
β’ ((πΊ β USPGraph β§ π β β0) β (β―β{π β (WalksβπΊ) β£ (β―β(1st βπ)) = π}) = (β―β(π WWalksN πΊ))) | ||
Theorem | wwlkseq 29409* | Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
β’ ((π β (WWalksβπΊ) β§ π β (WWalksβπΊ)) β (π = π β ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(πβπ) = (πβπ)))) | ||
Theorem | wwlksnred 29410 | Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
β’ (π β β0 β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (π WWalksN πΊ))) | ||
Theorem | wwlksnext 29411 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π β (π WWalksN πΊ) β§ π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ)) | ||
Theorem | wwlksnextbi 29412 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.) (Proof shortened by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((π β β0 β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β ((π + 1) WWalksN πΊ) β π β (π WWalksN πΊ))) | ||
Theorem | wwlksnredwwlkn 29413* | For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
β’ πΈ = (EdgβπΊ) β β’ (π β β0 β (π β ((π + 1) WWalksN πΊ) β βπ¦ β (π WWalksN πΊ)((π prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ)} β πΈ))) | ||
Theorem | wwlksnredwwlkn0 29414* | For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
β’ πΈ = (EdgβπΊ) β β’ ((π β β0 β§ π β ((π + 1) WWalksN πΊ)) β ((πβ0) = π β βπ¦ β (π WWalksN πΊ)((π prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ)} β πΈ))) | ||
Theorem | wwlksnextwrd 29415* | Lemma for wwlksnextbij 29420. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} β β’ (π β (π WWalksN πΊ) β π· = {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)}) | ||
Theorem | wwlksnextfun 29416* | Lemma for wwlksnextbij 29420. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} & β’ π = {π β π β£ {(lastSβπ), π} β πΈ} & β’ πΉ = (π‘ β π· β¦ (lastSβπ‘)) β β’ (π β β0 β πΉ:π·βΆπ ) | ||
Theorem | wwlksnextinj 29417* | Lemma for wwlksnextbij 29420. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} & β’ π = {π β π β£ {(lastSβπ), π} β πΈ} & β’ πΉ = (π‘ β π· β¦ (lastSβπ‘)) β β’ (π β β0 β πΉ:π·β1-1βπ ) | ||
Theorem | wwlksnextsurj 29418* | Lemma for wwlksnextbij 29420. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} & β’ π = {π β π β£ {(lastSβπ), π} β πΈ} & β’ πΉ = (π‘ β π· β¦ (lastSβπ‘)) β β’ (π β (π WWalksN πΊ) β πΉ:π·βontoβπ ) | ||
Theorem | wwlksnextbij0 29419* | Lemma for wwlksnextbij 29420. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Revised by AV, 18-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = {π€ β Word π β£ ((β―βπ€) = (π + 2) β§ (π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)} & β’ π = {π β π β£ {(lastSβπ), π} β πΈ} & β’ πΉ = (π‘ β π· β¦ (lastSβπ‘)) β β’ (π β (π WWalksN πΊ) β πΉ:π·β1-1-ontoβπ ) | ||
Theorem | wwlksnextbij 29420* | There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 18-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (π WWalksN πΊ) β βπ π:{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)}β1-1-ontoβ{π β π β£ {(lastSβπ), π} β πΈ}) | ||
Theorem | wwlksnexthasheq 29421* | The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (π WWalksN πΊ) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π β§ {(lastSβπ), (lastSβπ€)} β πΈ)}) = (β―β{π β π β£ {(lastSβπ), π} β πΈ})) | ||
Theorem | disjxwwlksn 29422* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Revised by AV, 27-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ Disj π¦ β (π WWalksN πΊ){π₯ β Word π β£ ((π₯ prefix π) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)} | ||
Theorem | wwlksnndef 29423 | Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) |
β’ ((πΊ β V β¨ π β β0) β (π WWalksN πΊ) = β ) | ||
Theorem | wwlksnfi 29424 | The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018.) (Revised by AV, 19-Apr-2021.) (Proof shortened by JJ, 18-Nov-2022.) |
β’ ((VtxβπΊ) β Fin β (π WWalksN πΊ) β Fin) | ||
Theorem | wlksnfi 29425* | The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 20-Apr-2021.) |
β’ ((πΊ β FinUSGraph β§ π β β0) β {π β (WalksβπΊ) β£ (β―β(1st βπ)) = π} β Fin) | ||
Theorem | wlksnwwlknvbij 29426* | There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 5-Aug-2022.) |
β’ ((πΊ β USPGraph β§ π β β0) β βπ π:{π β (WalksβπΊ) β£ ((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)}β1-1-ontoβ{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) | ||
Theorem | wwlksnextproplem1 29427 | Lemma 1 for wwlksnextprop 29430. (Contributed by Alexander van der Vekens, 31-Jul-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) β β’ ((π β π β§ π β β0) β ((π prefix (π + 1))β0) = (πβ0)) | ||
Theorem | wwlksnextproplem2 29428 | Lemma 2 for wwlksnextprop 29430. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π β π β§ π β β0) β {(lastSβ(π prefix (π + 1))), (lastSβπ)} β πΈ) | ||
Theorem | wwlksnextproplem3 29429* | Lemma 3 for wwlksnextprop 29430. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) & β’ πΈ = (EdgβπΊ) & β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β β’ ((π β π β§ (πβ0) = π β§ π β β0) β (π prefix (π + 1)) β π) | ||
Theorem | wwlksnextprop 29430* | Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 29-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) & β’ πΈ = (EdgβπΊ) & β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β β’ (π β β0 β {π₯ β π β£ (π₯β0) = π} = {π₯ β π β£ βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)}) | ||
Theorem | disjxwwlkn 29431* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) & β’ πΈ = (EdgβπΊ) & β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β β’ Disj π¦ β π {π₯ β π β£ ((π₯ prefix π) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)} | ||
Theorem | hashwwlksnext 29432* | Number of walks (as words) extended by an edge as a sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.) (Revised by AV, 20-Apr-2021.) (Revised by AV, 26-Oct-2022.) |
β’ π = ((π + 1) WWalksN πΊ) & β’ πΈ = (EdgβπΊ) & β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β β’ ((VtxβπΊ) β Fin β (β―β{π₯ β π β£ βπ¦ β π ((π₯ prefix π) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)}) = Ξ£π¦ β π (β―β{π₯ β π β£ ((π₯ prefix π) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)})) | ||
Theorem | wwlksnwwlksnon 29433* | A walk of fixed length is a walk of fixed length between two vertices. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 13-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π WWalksN πΊ) β βπ β π βπ β π π β (π(π WWalksNOn πΊ)π)) | ||
Theorem | wspthsnwspthsnon 29434* | A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-May-2021.) (Revised by AV, 13-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π WSPathsN πΊ) β βπ β π βπ β π π β (π(π WSPathsNOn πΊ)π)) | ||
Theorem | wspthsnonn0vne 29435 | If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.) |
β’ ((π β β β§ (π(π WSPathsNOn πΊ)π) β β ) β π β π) | ||
Theorem | wspthsswwlkn 29436 | The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length. (Contributed by AV, 18-May-2021.) |
β’ (π WSPathsN πΊ) β (π WWalksN πΊ) | ||
Theorem | wspthnfi 29437 | In a finite graph, the set of simple paths of a fixed length is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 18-May-2021.) |
β’ ((VtxβπΊ) β Fin β (π WSPathsN πΊ) β Fin) | ||
Theorem | wwlksnonfi 29438 | In a finite graph, the set of walks of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
β’ ((VtxβπΊ) β Fin β (π΄(π WWalksNOn πΊ)π΅) β Fin) | ||
Theorem | wspthsswwlknon 29439 | The set of simple paths of a fixed length between two vertices is a subset of the set of walks of the fixed length between the two vertices. (Contributed by AV, 15-May-2021.) |
β’ (π΄(π WSPathsNOn πΊ)π΅) β (π΄(π WWalksNOn πΊ)π΅) | ||
Theorem | wspthnonfi 29440 | In a finite graph, the set of simple paths of a fixed length between two vertices is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 15-May-2021.) |
β’ ((VtxβπΊ) β Fin β (π΄(π WSPathsNOn πΊ)π΅) β Fin) | ||
Theorem | wspniunwspnon 29441* | The set of nonempty simple paths of fixed length is the double union of the simple paths of the fixed length between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β β β§ πΊ β π) β (π WSPathsN πΊ) = βͺ π₯ β π βͺ π¦ β (π β {π₯})(π₯(π WSPathsNOn πΊ)π¦)) | ||
Theorem | wspn0 29442 | If there are no vertices, then there are no simple paths (of any length), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 16-May-2021.) (Proof shortened by AV, 13-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π = β β (π WSPathsN πΊ) = β ) | ||
Theorem | 2wlkdlem1 29443 | Lemma 1 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© β β’ (β―βπ) = ((β―βπΉ) + 1) | ||
Theorem | 2wlkdlem2 29444 | Lemma 2 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© β β’ (0..^(β―βπΉ)) = {0, 1} | ||
Theorem | 2wlkdlem3 29445 | Lemma 3 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) β β’ (π β ((πβ0) = π΄ β§ (πβ1) = π΅ β§ (πβ2) = πΆ)) | ||
Theorem | 2wlkdlem4 29446* | Lemma 4 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) β β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) | ||
Theorem | 2wlkdlem5 29447* | Lemma 5 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) β β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | 2pthdlem1 29448* | Lemma 1 for 2pthd 29458. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) β β’ (π β βπ β (0..^(β―βπ))βπ β (1..^(β―βπΉ))(π β π β (πβπ) β (πβπ))) | ||
Theorem | 2wlkdlem6 29449 | Lemma 6 for 2wlkd 29454. (Contributed by AV, 23-Jan-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β (π΅ β (πΌβπ½) β§ π΅ β (πΌβπΎ))) | ||
Theorem | 2wlkdlem7 29450 | Lemma 7 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β (π½ β V β§ πΎ β V)) | ||
Theorem | 2wlkdlem8 29451 | Lemma 8 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β ((πΉβ0) = π½ β§ (πΉβ1) = πΎ)) | ||
Theorem | 2wlkdlem9 29452 | Lemma 9 for 2wlkd 29454. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β ({π΄, π΅} β (πΌβ(πΉβ0)) β§ {π΅, πΆ} β (πΌβ(πΉβ1)))) | ||
Theorem | 2wlkdlem10 29453* | Lemma 10 for 3wlkd 29687. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) | ||
Theorem | 2wlkd 29454 | Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018.) (Revised by AV, 23-Jan-2021.) (Proof shortened by AV, 14-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(WalksβπΊ)π) | ||
Theorem | 2wlkond 29455 | A walk of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(π΄(WalksOnβπΊ)πΆ)π) | ||
Theorem | 2trld 29456 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β π½ β πΎ) β β’ (π β πΉ(TrailsβπΊ)π) | ||
Theorem | 2trlond 29457 | A trail of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β π½ β πΎ) β β’ (π β πΉ(π΄(TrailsOnβπΊ)πΆ)π) | ||
Theorem | 2pthd 29458 | A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β π½ β πΎ) β β’ (π β πΉ(PathsβπΊ)π) | ||
Theorem | 2spthd 29459 | A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 24-Jan-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β π½ β πΎ) & β’ (π β π΄ β πΆ) β β’ (π β πΉ(SPathsβπΊ)π) | ||
Theorem | 2pthond 29460 | A simple path of length 2 from one vertex to another, different vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 24-Jan-2021.) (Proof shortened by AV, 30-Jan-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β π½ β πΎ) & β’ (π β π΄ β πΆ) β β’ (π β πΉ(π΄(SPathsOnβπΊ)πΆ)π) | ||
Theorem | 2pthon3v 29461* | For a vertex adjacent to two other vertices there is a simple path of length 2 between these other vertices in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 24-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((πΊ β UHGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) β βπβπ(π(π΄(SPathsOnβπΊ)πΆ)π β§ (β―βπ) = 2)) | ||
Theorem | umgr2adedgwlklem 29462 | Lemma for umgr2adedgwlk 29463, umgr2adedgspth 29466, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ)))) | ||
Theorem | umgr2adedgwlk 29463 | In a multigraph, two adjacent edges form a walk of length 2. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = β¨βπ½πΎββ© & β’ π = β¨βπ΄π΅πΆββ© & β’ (π β πΊ β UMGraph) & β’ (π β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) & β’ (π β (πΌβπ½) = {π΄, π΅}) & β’ (π β (πΌβπΎ) = {π΅, πΆ}) β β’ (π β (πΉ(WalksβπΊ)π β§ (β―βπΉ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))) | ||
Theorem | umgr2adedgwlkon 29464 | In a multigraph, two adjacent edges form a walk between two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = β¨βπ½πΎββ© & β’ π = β¨βπ΄π΅πΆββ© & β’ (π β πΊ β UMGraph) & β’ (π β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) & β’ (π β (πΌβπ½) = {π΄, π΅}) & β’ (π β (πΌβπΎ) = {π΅, πΆ}) β β’ (π β πΉ(π΄(WalksOnβπΊ)πΆ)π) | ||
Theorem | umgr2adedgwlkonALT 29465 | Alternate proof for umgr2adedgwlkon 29464, using umgr2adedgwlk 29463, but with a much longer proof! In a multigraph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = β¨βπ½πΎββ© & β’ π = β¨βπ΄π΅πΆββ© & β’ (π β πΊ β UMGraph) & β’ (π β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) & β’ (π β (πΌβπ½) = {π΄, π΅}) & β’ (π β (πΌβπΎ) = {π΅, πΆ}) β β’ (π β πΉ(π΄(WalksOnβπΊ)πΆ)π) | ||
Theorem | umgr2adedgspth 29466 | In a multigraph, two adjacent edges with different endvertices form a simple path of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = β¨βπ½πΎββ© & β’ π = β¨βπ΄π΅πΆββ© & β’ (π β πΊ β UMGraph) & β’ (π β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ)) & β’ (π β (πΌβπ½) = {π΄, π΅}) & β’ (π β (πΌβπΎ) = {π΅, πΆ}) & β’ (π β π΄ β πΆ) β β’ (π β πΉ(SPathsβπΊ)π) | ||
Theorem | umgr2wlk 29467* | In a multigraph, there is a walk of length 2 for each pair of adjacent edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π΄ = (πβ0) β§ π΅ = (πβ1) β§ πΆ = (πβ2)))) | ||
Theorem | umgr2wlkon 29468* | For each pair of adjacent edges in a multigraph, there is a walk of length 2 between the not common vertices of the edges. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 30-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β βπβπ π(π΄(WalksOnβπΊ)πΆ)π) | ||
Theorem | elwwlks2s3 29469* | A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (2 WWalksN πΊ) β βπ β π βπ β π βπ β π π = β¨βπππββ©) | ||
Theorem | midwwlks2s3 29470* | There is a vertex between the endpoints of a walk of length 2 between two vertices as length 3 string. (Contributed by AV, 10-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (2 WWalksN πΊ) β βπ β π (πβ1) = π) | ||
Theorem | wwlks2onv 29471 | If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) (Proof shortened by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π΅ β π β§ β¨βπ΄π΅πΆββ© β (π΄(2 WWalksNOn πΊ)πΆ)) β (π΄ β π β§ π΅ β π β§ πΆ β π)) | ||
Theorem | elwwlks2ons3im 29472 | A walk as word of length 2 between two vertices is a length 3 string and its second symbol is a vertex. (Contributed by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π΄(2 WWalksNOn πΊ)πΆ) β (π = β¨βπ΄(πβ1)πΆββ© β§ (πβ1) β π)) | ||
Theorem | elwwlks2ons3 29473* | For each walk of length 2 between two vertices, there is a third vertex in the middle of the walk. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π΄(2 WWalksNOn πΊ)πΆ) β βπ β π (π = β¨βπ΄ππΆββ© β§ β¨βπ΄ππΆββ© β (π΄(2 WWalksNOn πΊ)πΆ))) | ||
Theorem | s3wwlks2on 29474* | A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ π΄ β π β§ πΆ β π) β (β¨βπ΄π΅πΆββ© β (π΄(2 WWalksNOn πΊ)πΆ) β βπ(π(WalksβπΊ)β¨βπ΄π΅πΆββ© β§ (β―βπ) = 2))) | ||
Theorem | umgrwwlks2on 29475 | A walk of length 2 between two vertices as word in a multigraph. This theorem would also hold for pseudographs, but to prove this the cases π΄ = π΅ and/or π΅ = πΆ must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (β¨βπ΄π΅πΆββ© β (π΄(2 WWalksNOn πΊ)πΆ) β ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ))) | ||
Theorem | wwlks2onsym 29476 | There is a walk of length 2 from one vertex to another vertex iff there is a walk of length 2 from the other vertex to the first vertex. (Contributed by AV, 7-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UMGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (β¨βπ΄π΅πΆββ© β (π΄(2 WWalksNOn πΊ)πΆ) β β¨βπΆπ΅π΄ββ© β (πΆ(2 WWalksNOn πΊ)π΄))) | ||
Theorem | elwwlks2on 29477* | A walk of length 2 between two vertices as length 3 string. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ π΄ β π β§ πΆ β π) β (π β (π΄(2 WWalksNOn πΊ)πΆ) β βπ β π (π = β¨βπ΄ππΆββ© β§ βπ(π(WalksβπΊ)π β§ (β―βπ) = 2)))) | ||
Theorem | elwspths2on 29478* | A simple path of length 2 between two vertices (in a graph) as length 3 string. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ π΄ β π β§ πΆ β π) β (π β (π΄(2 WSPathsNOn πΊ)πΆ) β βπ β π (π = β¨βπ΄ππΆββ© β§ β¨βπ΄ππΆββ© β (π΄(2 WSPathsNOn πΊ)πΆ)))) | ||
Theorem | wpthswwlks2on 29479 | For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 13-May-2021.) (Revised by AV, 16-Mar-2022.) |
β’ ((πΊ β USGraph β§ π΄ β π΅) β (π΄(2 WSPathsNOn πΊ)π΅) = (π΄(2 WWalksNOn πΊ)π΅)) | ||
Theorem | 2wspdisj 29480* | All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) (Revised by AV, 9-Jan-2022.) |
β’ Disj π β (π β {π΄})(π΄(2 WSPathsNOn πΊ)π) | ||
Theorem | 2wspiundisj 29481* | All simple paths of length 2 from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) (Revised by AV, 14-May-2021.) (Proof shortened by AV, 9-Jan-2022.) |
β’ Disj π β π βͺ π β (π β {π})(π(2 WSPathsNOn πΊ)π) | ||
Theorem | usgr2wspthons3 29482 | A simple path of length 2 between two vertices represented as length 3 string corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (β¨βπ΄π΅πΆββ© β (π΄(2 WSPathsNOn πΊ)πΆ) β (π΄ β πΆ β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ))) | ||
Theorem | usgr2wspthon 29483* | A simple path of length 2 between two vertices corresponds to two adjacent edges in a simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ (π΄ β π β§ πΆ β π)) β (π β (π΄(2 WSPathsNOn πΊ)πΆ) β βπ β π ((π = β¨βπ΄ππΆββ© β§ π΄ β πΆ) β§ ({π΄, π} β πΈ β§ {π, πΆ} β πΈ)))) | ||
Theorem | elwwlks2 29484* | A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (πΊ β UPGraph β (π β (2 WWalksN πΊ) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(WalksβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) | ||
Theorem | elwspths2spth 29485* | A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (πΊ β UPGraph β (π β (2 WSPathsN πΊ) β βπ β π βπ β π βπ β π (π = β¨βπππββ© β§ βπβπ(π(SPathsβπΊ)π β§ (β―βπ) = 2 β§ (π = (πβ0) β§ π = (πβ1) β§ π = (πβ2)))))) | ||
Theorem | rusgrnumwwlkl1 29486* | In a k-regular graph, there are k walks (as word) of length 1 starting at each vertex. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ π β π) β (β―β{π€ β (1 WWalksN πΊ) β£ (π€β0) = π}) = πΎ) | ||
Theorem | rusgrnumwwlkslem 29487* | Lemma for rusgrnumwwlks 29492. (Contributed by Alexander van der Vekens, 23-Aug-2018.) |
β’ (π β {π€ β π β£ (π€β0) = π} β {π€ β π β£ (π β§ π)} = {π€ β π β£ (π β§ (πβ0) = π β§ π)}) | ||
Theorem | rusgrnumwwlklem 29488* | Lemma for rusgrnumwwlk 29493 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 29489* | Induction base 0 for rusgrnumwwlk 29493. 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 29490* | Induction base 1 for rusgrnumwwlk 29493. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph πΎ β§ π β π) β (ππΏ1) = πΎ) | ||
Theorem | rusgr0edg 29491* | 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 29492* | Induction step for rusgrnumwwlk 29493. (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 29493* |
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 29494* | 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 29493. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) | ||
Theorem | rusgrnumwlkg 29495* | 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 29496* | 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 29497* | 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 29292: 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 14470, is also used in Definitions df-clwwlk 29499 and df-clwwlkn 29542, 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 29499, df-clwwlkn 29542 and df-clwwlknon 29605, 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 29648, 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 29559. Therefore, a closed walk corresponds to a closed walk as word only for walks of length at least 1, see clwlkclwwlk2 29520 or clwlkclwwlken 29529. 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 29545). 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 29605. This definition is also based on β0 instead of β, with (π(ClWWalksNOnβπΊ)0) = β (see clwwlk0on0 29609). clwwlknon1le1 29618 states that there is at most one (closed) walk of length 1 on a vertex, which would consist of a loop (see clwwlknon1loop 29615). And in a πΎ-regular graph, there are πΎ closed walks of length 2 on each vertex, see clwwlknon2num 29622. | ||
Syntax | cclwwlk 29498 | Extend class notation with closed walks (in an undirected graph) as word over the set of vertices. |
class ClWWalks | ||
Definition | df-clwwlk 29499* | 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 29292. 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 29500* | 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)} β πΈ)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |