![]() |
Metamath
Proof Explorer Theorem List (p. 293 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wwlksnextproplem1 29201 | Lemma 1 for wwlksnextprop 29204. (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 29202 | Lemma 2 for wwlksnextprop 29204. (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 29203* | Lemma 3 for wwlksnextprop 29204. (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 29204* | 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 29205* | 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 29206* | 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 29207* | 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 29208* | 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 29209 | 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 29210 | 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 29211 | 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 29212 | 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 29213 | 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 29214 | 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 29215* | 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 29216 | 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 29217 | Lemma 1 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© β β’ (β―βπ) = ((β―βπΉ) + 1) | ||
Theorem | 2wlkdlem2 29218 | Lemma 2 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© β β’ (0..^(β―βπΉ)) = {0, 1} | ||
Theorem | 2wlkdlem3 29219 | Lemma 3 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) β β’ (π β ((πβ0) = π΄ β§ (πβ1) = π΅ β§ (πβ2) = πΆ)) | ||
Theorem | 2wlkdlem4 29220* | Lemma 4 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) β β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) | ||
Theorem | 2wlkdlem5 29221* | Lemma 5 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) β β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | 2pthdlem1 29222* | Lemma 1 for 2pthd 29232. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) β β’ (π β βπ β (0..^(β―βπ))βπ β (1..^(β―βπΉ))(π β π β (πβπ) β (πβπ))) | ||
Theorem | 2wlkdlem6 29223 | Lemma 6 for 2wlkd 29228. (Contributed by AV, 23-Jan-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β (π΅ β (πΌβπ½) β§ π΅ β (πΌβπΎ))) | ||
Theorem | 2wlkdlem7 29224 | Lemma 7 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β (π½ β V β§ πΎ β V)) | ||
Theorem | 2wlkdlem8 29225 | Lemma 8 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β ((πΉβ0) = π½ β§ (πΉβ1) = πΎ)) | ||
Theorem | 2wlkdlem9 29226 | Lemma 9 for 2wlkd 29228. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β ({π΄, π΅} β (πΌβ(πΉβ0)) β§ {π΅, πΆ} β (πΌβ(πΉβ1)))) | ||
Theorem | 2wlkdlem10 29227* | Lemma 10 for 3wlkd 29461. (Contributed by AV, 14-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆββ© & β’ πΉ = β¨βπ½πΎββ© & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β (π΄ β π΅ β§ π΅ β πΆ)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ))) β β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) | ||
Theorem | 2wlkd 29228 | 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 29229 | 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 29230 | 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 29231 | 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 29232 | 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 29233 | 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 29234 | 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 29235* | 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 29236 | Lemma for umgr2adedgwlk 29237, umgr2adedgspth 29240, etc. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 29-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β ((π΄ β π΅ β§ π΅ β πΆ) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ) β§ πΆ β (VtxβπΊ)))) | ||
Theorem | umgr2adedgwlk 29237 | 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 29238 | 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 29239 | Alternate proof for umgr2adedgwlkon 29238, using umgr2adedgwlk 29237, 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 29240 | 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 29241* | 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 29242* | 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 29243* | A walk of length 2 as word is a length 3 string. (Contributed by AV, 18-May-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (2 WWalksN πΊ) β βπ β π βπ β π βπ β π π = β¨βπππββ©) | ||
Theorem | midwwlks2s3 29244* | 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 29245 | 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 29246 | 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 29247* | 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 29248* | 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 29249 | 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 29250 | 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 29251* | 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 29252* | 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 29253 | 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 29254* | 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 29255* | 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 29256 | 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 29257* | 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 29258* | 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 29259* | 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 29260* | 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 29261* | Lemma for rusgrnumwwlks 29266. (Contributed by Alexander van der Vekens, 23-Aug-2018.) |
β’ (π β {π€ β π β£ (π€β0) = π} β {π€ β π β£ (π β§ π)} = {π€ β π β£ (π β§ (πβ0) = π β§ π)}) | ||
Theorem | rusgrnumwwlklem 29262* | Lemma for rusgrnumwwlk 29267 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 29263* | Induction base 0 for rusgrnumwwlk 29267. 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 29264* | Induction base 1 for rusgrnumwwlk 29267. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΏ = (π£ β π, π β β0 β¦ (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π£})) β β’ ((πΊ RegUSGraph πΎ β§ π β π) β (ππΏ1) = πΎ) | ||
Theorem | rusgr0edg 29265* | 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 29266* | Induction step for rusgrnumwwlk 29267. (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 29267* |
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 29268* | 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 29267. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) | ||
Theorem | rusgrnumwlkg 29269* | 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 29270* | 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 29271* | 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 29066: 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 14467, is also used in Definitions df-clwwlk 29273 and df-clwwlkn 29316, 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 29273, df-clwwlkn 29316 and df-clwwlknon 29379, 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 29422, 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 29333. Therefore, a closed walk corresponds to a closed walk as word only for walks of length at least 1, see clwlkclwwlk2 29294 or clwlkclwwlken 29303. 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 29319). 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 29379. This definition is also based on β0 instead of β, with (π(ClWWalksNOnβπΊ)0) = β (see clwwlk0on0 29383). clwwlknon1le1 29392 states that there is at most one (closed) walk of length 1 on a vertex, which would consist of a loop (see clwwlknon1loop 29389). And in a πΎ-regular graph, there are πΎ closed walks of length 2 on each vertex, see clwwlknon2num 29396. | ||
Syntax | cclwwlk 29272 | Extend class notation with closed walks (in an undirected graph) as word over the set of vertices. |
class ClWWalks | ||
Definition | df-clwwlk 29273* | 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 29066. 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 29274* | 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 29275* | 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 29276 | 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 29277 | 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 29278 | 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 29279 | A closed walk of length 1 is a loop. See also clwlkl1loop 29078. (Contributed by AV, 24-Apr-2021.) |
β’ ((π β (ClWWalksβπΊ) β§ (β―βπ) = 1) β {(πβ0), (πβ0)} β (EdgβπΊ)) | ||
Theorem | clwwlkccatlem 29280* | Lemma for clwwlkccat 29281: 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 29281 | 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 29282 | 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 29283* | Lemma 1 for clwlkclwwlklem2a 29289. (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 29284* | Lemma 2 for clwlkclwwlklem2a 29289. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) | ||
Theorem | clwlkclwwlklem2a3 29285* | Lemma 3 for clwlkclwwlklem2a 29289. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ ((π β Word π β§ 2 β€ (β―βπ)) β (πβ(β―βπΉ)) = (lastSβπ)) | ||
Theorem | clwlkclwwlklem2fv1 29286* | Lemma 4a for clwlkclwwlklem2a 29289. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ (((β―βπ) β β0 β§ πΌ β (0..^((β―βπ) β 2))) β (πΉβπΌ) = (β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) | ||
Theorem | clwlkclwwlklem2fv2 29287* | Lemma 4b for clwlkclwwlklem2a 29289. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ if(π₯ < ((β―βπ) β 2), (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))}), (β‘πΈβ{(πβπ₯), (πβ0)}))) β β’ (((β―βπ) β β0 β§ 2 β€ (β―βπ)) β (πΉβ((β―βπ) β 2)) = (β‘πΈβ{(πβ((β―βπ) β 2)), (πβ0)})) | ||
Theorem | clwlkclwwlklem2a4 29288* | Lemma 4 for clwlkclwwlklem2a 29289. (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 29289* | Lemma for clwlkclwwlklem2 29291. (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 29290* | Lemma 1 for clwlkclwwlk 29293. (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 29291* | Lemma 2 for clwlkclwwlk 29293. (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 29292* | Lemma 3 for clwlkclwwlk 29293. (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 29293* | 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 29294* | 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 29295* | Lemma for clwlkclwwlkf 29299. (Contributed by AV, 24-May-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) β β’ (π β πΆ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) | ||
Theorem | clwlkclwwlkf1lem2 29296* | Lemma 2 for clwlkclwwlkf1 29301. (Contributed by AV, 24-May-2022.) (Revised by AV, 30-Oct-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} & β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) & β’ π· = (1st βπ) & β’ πΈ = (2nd βπ) β β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) | ||
Theorem | clwlkclwwlkf1lem3 29297* | Lemma 3 for clwlkclwwlkf1 29301. (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 29298* | Lemma for clwlkclwwlkfo 29300. (Contributed by AV, 25-May-2022.) |
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€ (β―β(1st βπ€))} β β’ ((π β Word (VtxβπΊ) β§ 1 β€ (β―βπ) β§ β¨π, (π ++ β¨β(πβ0)ββ©)β© β (ClWalksβπΊ)) β β¨π, (π ++ β¨β(πβ0)ββ©)β© β πΆ) | ||
Theorem | clwlkclwwlkf 29299* | πΉ 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 29300* | πΉ 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βπΊ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |