![]() |
Metamath
Proof Explorer Theorem List (p. 290 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wlkvtxedg 28901* | The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ (πΉ(WalksβπΊ)π β βπ β (0..^(β―βπΉ))βπ β πΈ {(πβπ), (πβ(π + 1))} β π) | ||
Theorem | upgrwlkvtxedg 28902* | The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β πΈ) | ||
Theorem | uspgr2wlkeq 28903* | Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.) |
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ π = (β―β(1st βπ΄))) β (π΄ = π΅ β (π = (β―β(1st βπ΅)) β§ βπ¦ β (0...π)((2nd βπ΄)βπ¦) = ((2nd βπ΅)βπ¦)))) | ||
Theorem | uspgr2wlkeq2 28904 | Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
β’ (((πΊ β USPGraph β§ π β β0) β§ (π΄ β (WalksβπΊ) β§ (β―β(1st βπ΄)) = π) β§ (π΅ β (WalksβπΊ) β§ (β―β(1st βπ΅)) = π)) β ((2nd βπ΄) = (2nd βπ΅) β π΄ = π΅)) | ||
Theorem | uspgr2wlkeqi 28905 | Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021.) |
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ (2nd βπ΄) = (2nd βπ΅)) β π΄ = π΅) | ||
Theorem | umgrwlknloop 28906* | In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.) |
β’ ((πΊ β UMGraph β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | wlkResOLD 28907* | Obsolete version of opabresex2 7461 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 30-Dec-2020.) (Proof shortened by AV, 15-Jan-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π(πβπΊ)π β π(WalksβπΊ)π) β β’ {β¨π, πβ© β£ (π(πβπΊ)π β§ π)} β V | ||
Theorem | wlkv0 28908 | If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
β’ (((VtxβπΊ) = β β§ π β (WalksβπΊ)) β ((1st βπ) = β β§ (2nd βπ) = β )) | ||
Theorem | g0wlk0 28909 | There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
β’ ((VtxβπΊ) = β β (WalksβπΊ) = β ) | ||
Theorem | 0wlk0 28910 | There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
β’ (Walksββ ) = β | ||
Theorem | wlk0prc 28911 | There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
β’ ((π β V β§ (Vtxβπ) = (VtxβπΊ)) β (WalksβπΊ) = β ) | ||
Theorem | wlklenvclwlk 28912 | The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by JJ, 14-Jan-2024.) |
β’ (π β Word (VtxβπΊ) β (β¨πΉ, (π ++ β¨β(πβ0)ββ©)β© β (WalksβπΊ) β (β―βπΉ) = (β―βπ))) | ||
Theorem | wlkson 28913* | The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 30-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π΄ β π β§ π΅ β π) β (π΄(WalksOnβπΊ)π΅) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπ)) = π΅)}) | ||
Theorem | iswlkon 28914 | Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 31-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β π β§ π β π)) β (πΉ(π΄(WalksOnβπΊ)π΅)π β (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) | ||
Theorem | wlkonprop 28915 | Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 31-Dec-2020.) (Proof shortened by AV, 16-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) | ||
Theorem | wlkpvtx 28916 | A walk connects vertices. (Contributed by AV, 22-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(WalksβπΊ)π β (π β (0...(β―βπΉ)) β (πβπ) β π)) | ||
Theorem | wlkepvtx 28917 | The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(WalksβπΊ)π β ((πβ0) β π β§ (πβ(β―βπΉ)) β π)) | ||
Theorem | wlkoniswlk 28918 | A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 2-Jan-2021.) |
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(WalksβπΊ)π) | ||
Theorem | wlkonwlk 28919 | A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.) |
β’ (πΉ(WalksβπΊ)π β πΉ((πβ0)(WalksOnβπΊ)(πβ(β―βπΉ)))π) | ||
Theorem | wlkonwlk1l 28920 | A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 22-Mar-2021.) |
β’ (π β πΉ(WalksβπΊ)π) β β’ (π β πΉ((πβ0)(WalksOnβπΊ)(lastSβπ))π) | ||
Theorem | wlksoneq1eq2 28921 | Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.) |
β’ ((πΉ(π΄(WalksOnβπΊ)π΅)π β§ π»(πΆ(WalksOnβπΊ)π·)π) β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | wlkonl1iedg 28922* | If there is a walk between two vertices π΄ and π΅ at least of length 1, then the start vertex π΄ is incident with an edge. (Contributed by AV, 4-Apr-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ(π΄(WalksOnβπΊ)π΅)π β§ (β―βπΉ) β 0) β βπ β ran πΌ π΄ β π) | ||
Theorem | wlkon2n0 28923 | The length of a walk between two different vertices is not 0 (i.e. is at least 1). (Contributed by AV, 3-Apr-2021.) |
β’ ((πΉ(π΄(WalksOnβπΊ)π΅)π β§ π΄ β π΅) β (β―βπΉ) β 0) | ||
Theorem | 2wlklem 28924* | Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
β’ (βπ β {0, 1} (πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΈβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΈβ(πΉβ1)) = {(πβ1), (πβ2)})) | ||
Theorem | upgr2wlk 28925 | Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 28-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) | ||
Theorem | wlkreslem 28926 | Lemma for wlkres 28927. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(WalksβπΊ)π) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β (Vtxβπ) = π) β β’ (π β π β V) | ||
Theorem | wlkres 28927 | The restriction β¨π», πβ© of a walk β¨πΉ, πβ© to an initial segment of the walk (of length π) forms a walk on the subgraph π consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 29468. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(WalksβπΊ)π) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ π» = (πΉ prefix π) & β’ π = (π βΎ (0...π)) β β’ (π β π»(Walksβπ)π) | ||
Theorem | redwlklem 28928 | Lemma for redwlk 28929. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
β’ ((πΉ β Word π β§ 1 β€ (β―βπΉ) β§ π:(0...(β―βπΉ))βΆπ) β (π βΎ (0..^(β―βπΉ))):(0...(β―β(πΉ βΎ (0..^((β―βπΉ) β 1)))))βΆπ) | ||
Theorem | redwlk 28929 | A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ 1 β€ (β―βπΉ)) β (πΉ βΎ (0..^((β―βπΉ) β 1)))(WalksβπΊ)(π βΎ (0..^(β―βπΉ)))) | ||
Theorem | wlkp1lem1 28930 | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) β β’ (π β Β¬ (π + 1) β dom π) | ||
Theorem | wlkp1lem2 28931 | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) β β’ (π β (β―βπ») = (π + 1)) | ||
Theorem | wlkp1lem3 28932 | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) β β’ (π β ((iEdgβπ)β(π»βπ)) = ((πΌ βͺ {β¨π΅, πΈβ©})βπ΅)) | ||
Theorem | wlkp1lem4 28933 | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) β β’ (π β (π β V β§ π» β V β§ π β V)) | ||
Theorem | wlkp1lem5 28934* | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) β β’ (π β βπ β (0...π)(πβπ) = (πβπ)) | ||
Theorem | wlkp1lem6 28935* | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) β β’ (π β βπ β (0..^π)((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ)))) | ||
Theorem | wlkp1lem7 28936 | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) β β’ (π β {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) | ||
Theorem | wlkp1lem8 28937* | Lemma for wlkp1 28938. (Contributed by AV, 6-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) & β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) β β’ (π β βπ β (0..^(β―βπ»))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))) | ||
Theorem | wlkp1 28938 | Append one path segment (edge) πΈ from vertex (πβπ) to a vertex πΆ to a walk β¨πΉ, πβ© to become a walk β¨π», πβ© of the supergraph π obtained by adding the new edge to the graph πΊ. Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 29469. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 6-Mar-2021.) (Proof shortened by AV, 18-Apr-2021.) (Revised by AV, 8-Apr-2024.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(WalksβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (π β (Vtxβπ) = π) & β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) β β’ (π β π»(Walksβπ)π) | ||
Theorem | wlkdlem1 28939* | Lemma 1 for wlkd 28943. (Contributed by AV, 7-Feb-2021.) |
β’ (π β π β Word V) & β’ (π β πΉ β Word V) & β’ (π β (β―βπ) = ((β―βπΉ) + 1)) & β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) β β’ (π β π:(0...(β―βπΉ))βΆπ) | ||
Theorem | wlkdlem2 28940* | Lemma 2 for wlkd 28943. (Contributed by AV, 7-Feb-2021.) |
β’ (π β π β Word V) & β’ (π β πΉ β Word V) & β’ (π β (β―βπ) = ((β―βπΉ) + 1)) & β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β β’ (π β (((β―βπΉ) β β β (πβ(β―βπΉ)) β (πΌβ(πΉβ((β―βπΉ) β 1)))) β§ βπ β (0..^(β―βπΉ))(πβπ) β (πΌβ(πΉβπ)))) | ||
Theorem | wlkdlem3 28941* | Lemma 3 for wlkd 28943. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ (π β π β Word V) & β’ (π β πΉ β Word V) & β’ (π β (β―βπ) = ((β―βπΉ) + 1)) & β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β β’ (π β πΉ β Word dom πΌ) | ||
Theorem | wlkdlem4 28942* | Lemma 4 for wlkd 28943. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.) |
β’ (π β π β Word V) & β’ (π β πΉ β Word V) & β’ (π β (β―βπ) = ((β―βπΉ) + 1)) & β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) & β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) β β’ (π β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) | ||
Theorem | wlkd 28943* | Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.) |
β’ (π β π β Word V) & β’ (π β πΉ β Word V) & β’ (π β (β―βπ) = ((β―βπΉ) + 1)) & β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) & β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) & β’ (π β πΊ β π) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) β β’ (π β πΉ(WalksβπΊ)π) | ||
Theorem | lfgrwlkprop 28944* | Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ(WalksβπΊ)π β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | lfgriswlk 28945* | Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β π β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))((πβπ) β (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) | ||
Theorem | lfgrwlknloop 28946* | In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β§ πΉ(WalksβπΊ)π) β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Syntax | ctrls 28947 | Extend class notation with trails (within a graph). |
class Trails | ||
Syntax | ctrlson 28948 | Extend class notation with trails between two vertices (within a graph). |
class TrailsOn | ||
Definition | df-trls 28949* |
Define the set of all Trails (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ Trails = (π β V β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ Fun β‘π)}) | ||
Definition | df-trlson 28950* | Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ TrailsOn = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(π(WalksOnβπ)π)π β§ π(Trailsβπ)π)})) | ||
Theorem | reltrls 28951 | The set (TrailsβπΊ) of all trails on πΊ is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.) |
β’ Rel (TrailsβπΊ) | ||
Theorem | trlsfval 28952* | The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.) |
β’ (TrailsβπΊ) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ Fun β‘π)} | ||
Theorem | istrl 28953 | Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.) |
β’ (πΉ(TrailsβπΊ)π β (πΉ(WalksβπΊ)π β§ Fun β‘πΉ)) | ||
Theorem | trliswlk 28954 | A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.) |
β’ (πΉ(TrailsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | trlf1 28955 | The enumeration πΉ of a trail β¨πΉ, πβ© is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(TrailsβπΊ)π β πΉ:(0..^(β―βπΉ))β1-1βdom πΌ) | ||
Theorem | trlreslem 28956 | Lemma for trlres 28957. Formerly part of proof of eupthres 29468. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β π β (0..^(β―βπΉ))) & β’ π» = (πΉ prefix π) β β’ (π β π»:(0..^(β―βπ»))β1-1-ontoβdom (πΌ βΎ (πΉ β (0..^π)))) | ||
Theorem | trlres 28957 | The restriction β¨π», πβ© of a trail β¨πΉ, πβ© to an initial segment of the trail (of length π) forms a trail on the subgraph π consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β π β (0..^(β―βπΉ))) & β’ π» = (πΉ prefix π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ π = (π βΎ (0...π)) β β’ (π β π»(Trailsβπ)π) | ||
Theorem | upgrtrls 28958* | The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β (TrailsβπΊ) = {β¨π, πβ© β£ ((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) | ||
Theorem | upgristrl 28959* | Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β (πΉ(TrailsβπΊ)π β ((πΉ β Word dom πΌ β§ Fun β‘πΉ) β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upgrf1istrl 28960* | Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β (πΉ(TrailsβπΊ)π β (πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | wksonproplem 28961* | Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 28965. (Contributed by AV, 16-Jan-2021.) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024.) |
β’ π = (VtxβπΊ) & β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(πβπΊ)π΅)π β (πΉ(π΄(πβπΊ)π΅)π β§ πΉ(πβπΊ)π))) & β’ π = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(π(πβπ)π)π β§ π(πβπ)π)})) β β’ (πΉ(π΄(πβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(π΄(πβπΊ)π΅)π β§ πΉ(πβπΊ)π))) | ||
Theorem | wksonproplemOLD 28962* | Obsolete version of wksonproplem 28961 as of 13-Dec-2024. (Contributed by AV, 16-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (VtxβπΊ) & β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(πβπΊ)π΅)π β (πΉ(π΄(πβπΊ)π΅)π β§ πΉ(πβπΊ)π))) & β’ π = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(π(πβπ)π)π β§ π(πβπ)π)})) & β’ (((πΊ β V β§ π΄ β π β§ π΅ β π) β§ π(πβπΊ)π) β π(WalksβπΊ)π) β β’ (πΉ(π΄(πβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(π΄(πβπΊ)π΅)π β§ πΉ(πβπΊ)π))) | ||
Theorem | trlsonfval 28963* | The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π΄ β π β§ π΅ β π) β (π΄(TrailsOnβπΊ)π΅) = {β¨π, πβ© β£ (π(π΄(WalksOnβπΊ)π΅)π β§ π(TrailsβπΊ)π)}) | ||
Theorem | istrlson 28964 | Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β π β§ π β π)) β (πΉ(π΄(TrailsOnβπΊ)π΅)π β (πΉ(π΄(WalksOnβπΊ)π΅)π β§ πΉ(TrailsβπΊ)π))) | ||
Theorem | trlsonprop 28965 | Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(π΄(TrailsOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(π΄(WalksOnβπΊ)π΅)π β§ πΉ(TrailsβπΊ)π))) | ||
Theorem | trlsonistrl 28966 | A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.) |
β’ (πΉ(π΄(TrailsOnβπΊ)π΅)π β πΉ(TrailsβπΊ)π) | ||
Theorem | trlsonwlkon 28967 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) |
β’ (πΉ(π΄(TrailsOnβπΊ)π΅)π β πΉ(π΄(WalksOnβπΊ)π΅)π) | ||
Theorem | trlontrl 28968 | A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.) |
β’ (πΉ(TrailsβπΊ)π β πΉ((πβ0)(TrailsOnβπΊ)(πβ(β―βπΉ)))π) | ||
Syntax | cpths 28969 | Extend class notation with paths (of a graph). |
class Paths | ||
Syntax | cspths 28970 | Extend class notation with simple paths (of a graph). |
class SPaths | ||
Syntax | cpthson 28971 | Extend class notation with paths between two vertices (within a graph). |
class PathsOn | ||
Syntax | cspthson 28972 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathsOn | ||
Definition | df-pths 28973* |
Define the set of all paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 28996). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
β’ Paths = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β )}) | ||
Definition | df-spths 28974* |
Define the set of all simple paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
β’ SPaths = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ Fun β‘π)}) | ||
Definition | df-pthson 28975* | Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
β’ PathsOn = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(π(TrailsOnβπ)π)π β§ π(Pathsβπ)π)})) | ||
Definition | df-spthson 28976* | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.) |
β’ SPathsOn = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(π(TrailsOnβπ)π)π β§ π(SPathsβπ)π)})) | ||
Theorem | relpths 28977 | The set (PathsβπΊ) of all paths on πΊ is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.) |
β’ Rel (PathsβπΊ) | ||
Theorem | pthsfval 28978* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ (PathsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β )} | ||
Theorem | spthsfval 28979* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ (SPathsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ Fun β‘π)} | ||
Theorem | ispth 28980 | Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ (πΉ(PathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β )) | ||
Theorem | isspth 28981 | Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
β’ (πΉ(SPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) | ||
Theorem | pthistrl 28982 | A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(PathsβπΊ)π β πΉ(TrailsβπΊ)π) | ||
Theorem | spthispth 28983 | A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(SPathsβπΊ)π β πΉ(PathsβπΊ)π) | ||
Theorem | pthiswlk 28984 | A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | spthiswlk 28985 | A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
β’ (πΉ(SPathsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | pthdivtx 28986 | The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ ((πΉ(PathsβπΊ)π β§ (πΌ β (1..^(β―βπΉ)) β§ π½ β (0...(β―βπΉ)) β§ πΌ β π½)) β (πβπΌ) β (πβπ½)) | ||
Theorem | pthdadjvtx 28987 | The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.) |
β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ) β§ πΌ β (0..^(β―βπΉ))) β (πβπΌ) β (πβ(πΌ + 1))) | ||
Theorem | 2pthnloop 28988* | A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 29404. (Contributed by AV, 6-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β (0..^(β―βπΉ))2 β€ (β―β(πΌβ(πΉβπ)))) | ||
Theorem | upgr2pthnlp 28989* | A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β (0..^(β―βπΉ))(β―β(πΌβ(πΉβπ))) = 2) | ||
Theorem | spthdifv 28990 | The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(SPathsβπΊ)π β π:(0...(β―βπΉ))β1-1β(VtxβπΊ)) | ||
Theorem | spthdep 28991 | A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ ((πΉ(SPathsβπΊ)π β§ (β―βπΉ) β 0) β (πβ0) β (πβ(β―βπΉ))) | ||
Theorem | pthdepisspth 28992 | A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) β (πβ(β―βπΉ))) β πΉ(SPathsβπΊ)π) | ||
Theorem | upgrwlkdvdelem 28993* | Lemma for upgrwlkdvde 28994. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.) |
β’ ((π:(0...(β―βπΉ))β1-1βπ β§ πΉ β Word dom πΌ) β (βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β Fun β‘πΉ)) | ||
Theorem | upgrwlkdvde 28994 | In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 28995. (Contributed by AV, 17-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π β§ Fun β‘π) β Fun β‘πΉ) | ||
Theorem | upgrspthswlk 28995* | The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΊ β UPGraph β (SPathsβπΊ) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ Fun β‘π)}) | ||
Theorem | upgrwlkdvspth 28996 | A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 28995. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π β§ Fun β‘π) β πΉ(SPathsβπΊ)π) | ||
Theorem | pthsonfval 28997* | The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π΄ β π β§ π΅ β π) β (π΄(PathsOnβπΊ)π΅) = {β¨π, πβ© β£ (π(π΄(TrailsOnβπΊ)π΅)π β§ π(PathsβπΊ)π)}) | ||
Theorem | spthson 28998* | The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π΄ β π β§ π΅ β π) β (π΄(SPathsOnβπΊ)π΅) = {β¨π, πβ© β£ (π(π΄(TrailsOnβπΊ)π΅)π β§ π(SPathsβπΊ)π)}) | ||
Theorem | ispthson 28999 | Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β π β§ π β π)) β (πΉ(π΄(PathsOnβπΊ)π΅)π β (πΉ(π΄(TrailsOnβπΊ)π΅)π β§ πΉ(PathsβπΊ)π))) | ||
Theorem | isspthson 29000 | Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β π β§ π β π)) β (πΉ(π΄(SPathsOnβπΊ)π΅)π β (πΉ(π΄(TrailsOnβπΊ)π΅)π β§ πΉ(SPathsβπΊ)π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |