![]() |
Metamath
Proof Explorer Theorem List (p. 296 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trlres 29501 | 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 29502* | 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 29503* | 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 29504* | 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 29505* | Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 29509. (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 29506* | Obsolete version of wksonproplem 29505 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 29507* | 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 29508 | 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 29509 | 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 29510 | 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 29511 | 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 29512 | A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.) |
β’ (πΉ(TrailsβπΊ)π β πΉ((πβ0)(TrailsOnβπΊ)(πβ(β―βπΉ)))π) | ||
Syntax | cpths 29513 | Extend class notation with paths (of a graph). |
class Paths | ||
Syntax | cspths 29514 | Extend class notation with simple paths (of a graph). |
class SPaths | ||
Syntax | cpthson 29515 | Extend class notation with paths between two vertices (within a graph). |
class PathsOn | ||
Syntax | cspthson 29516 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathsOn | ||
Definition | df-pths 29517* |
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 29540). 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 29518* |
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 29519* | 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 29520* | 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 29521 | 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 29522* | 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 29523* | 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 29524 | 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 29525 | 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 29526 | 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 29527 | 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 29528 | A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
β’ (πΉ(PathsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | spthiswlk 29529 | A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
β’ (πΉ(SPathsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | pthdivtx 29530 | 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 29531 | 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 29532* | 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 29948. (Contributed by AV, 6-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ(PathsβπΊ)π β§ 1 < (β―βπΉ)) β βπ β (0..^(β―βπΉ))2 β€ (β―β(πΌβ(πΉβπ)))) | ||
Theorem | upgr2pthnlp 29533* | 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 29534 | 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 29535 | 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 29536 | 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 29537* | Lemma for upgrwlkdvde 29538. (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 29538 | 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 29539. (Contributed by AV, 17-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π β§ Fun β‘π) β Fun β‘πΉ) | ||
Theorem | upgrspthswlk 29539* | 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 29540 | 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 29539. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π β§ Fun β‘π) β πΉ(SPathsβπΊ)π) | ||
Theorem | pthsonfval 29541* | 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 29542* | 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 29543 | 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 29544 | 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βπΊ)π))) | ||
Theorem | pthsonprop 29545 | Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(π΄(TrailsOnβπΊ)π΅)π β§ πΉ(PathsβπΊ)π))) | ||
Theorem | spthonprop 29546 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β π β§ π΅ β π) β§ (πΉ β V β§ π β V) β§ (πΉ(π΄(TrailsOnβπΊ)π΅)π β§ πΉ(SPathsβπΊ)π))) | ||
Theorem | pthonispth 29547 | A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.) |
β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β πΉ(PathsβπΊ)π) | ||
Theorem | pthontrlon 29548 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β πΉ(π΄(TrailsOnβπΊ)π΅)π) | ||
Theorem | pthonpth 29549 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
β’ (πΉ(PathsβπΊ)π β πΉ((πβ0)(PathsOnβπΊ)(πβ(β―βπΉ)))π) | ||
Theorem | isspthonpth 29550 | A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (((π΄ β π β§ π΅ β π) β§ (πΉ β π β§ π β π)) β (πΉ(π΄(SPathsOnβπΊ)π΅)π β (πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) | ||
Theorem | spthonisspth 29551 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.) |
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(SPathsβπΊ)π) | ||
Theorem | spthonpthon 29552 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(PathsOnβπΊ)π΅)π) | ||
Theorem | spthonepeq 29553 | The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β (π΄ = π΅ β (β―βπΉ) = 0)) | ||
Theorem | uhgrwkspthlem1 29554 | Lemma 1 for uhgrwkspth 29556. (Contributed by AV, 25-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 1) β Fun β‘πΉ) | ||
Theorem | uhgrwkspthlem2 29555 | Lemma 2 for uhgrwkspth 29556. (Contributed by AV, 25-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ ((β―βπΉ) = 1 β§ π΄ β π΅) β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β Fun β‘π) | ||
Theorem | uhgrwkspth 29556 | Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.) |
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(π΄(SPathsOnβπΊ)π΅)π)) | ||
Theorem | usgr2wlkneq 29557 | The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
β’ (((πΊ β USGraph β§ πΉ(WalksβπΊ)π) β§ ((β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β (((πβ0) β (πβ1) β§ (πβ0) β (πβ2) β§ (πβ1) β (πβ2)) β§ (πΉβ0) β (πΉβ1))) | ||
Theorem | usgr2wlkspthlem1 29558 | Lemma 1 for usgr2wlkspth 29560. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘πΉ) | ||
Theorem | usgr2wlkspthlem2 29559 | Lemma 2 for usgr2wlkspth 29560. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘π) | ||
Theorem | usgr2wlkspth 29560 | In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2 β§ π΄ β π΅) β (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(π΄(SPathsOnβπΊ)π΅)π)) | ||
Theorem | usgr2trlncl 29561 | In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2) β (πΉ(TrailsβπΊ)π β (πβ0) β (πβ2))) | ||
Theorem | usgr2trlspth 29562 | In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2) β (πΉ(TrailsβπΊ)π β πΉ(SPathsβπΊ)π)) | ||
Theorem | usgr2pthspth 29563 | In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2) β (πΉ(PathsβπΊ)π β πΉ(SPathsβπΊ)π)) | ||
Theorem | usgr2pthlem 29564* | Lemma for usgr2pth 29565. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΉ:(0..^(β―βπΉ))β1-1βdom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β ((πΊ β USGraph β§ (β―βπΉ) = 2) β βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§})))) | ||
Theorem | usgr2pth 29565* | In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β USGraph β ((πΉ(PathsβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π¦ β§ (πβ2) = π§) β§ ((πΌβ(πΉβ0)) = {π₯, π¦} β§ (πΌβ(πΉβ1)) = {π¦, π§}))))) | ||
Theorem | usgr2pth0 29566* | In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β USGraph β ((πΉ(PathsβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)β1-1βdom πΌ β§ π:(0...2)β1-1βπ β§ βπ₯ β π βπ¦ β (π β {π₯})βπ§ β (π β {π₯, π¦})(((πβ0) = π₯ β§ (πβ1) = π§ β§ (πβ2) = π¦) β§ ((πΌβ(πΉβ0)) = {π₯, π§} β§ (πΌβ(πΉβ1)) = {π§, π¦}))))) | ||
Theorem | pthdlem1 29567* | Lemma 1 for pthd 29570. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ (π β Fun β‘(π βΎ (1..^π ))) | ||
Theorem | pthdlem2lem 29568* | Lemma for pthdlem2 29569. (Contributed by AV, 10-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ ((π β§ (β―βπ) β β β§ (πΌ = 0 β¨ πΌ = π )) β (πβπΌ) β (π β (1..^π ))) | ||
Theorem | pthdlem2 29569* | Lemma 2 for pthd 29570. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ (π β ((π β {0, π }) β© (π β (1..^π ))) = β ) | ||
Theorem | pthd 29570* | Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) & β’ (β―βπΉ) = π & β’ (π β πΉ(TrailsβπΊ)π) β β’ (π β πΉ(PathsβπΊ)π) | ||
Syntax | cclwlks 29571 | Extend class notation with closed walks (of a graph). |
class ClWalks | ||
Definition | df-clwlks 29572* |
Define the set of all closed walks (in an undirected graph).
According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex can be considered as a closed walk of length 0, see also 0clwlk 29927. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
β’ ClWalks = (π β V β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Theorem | clwlks 29573* | The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Revised by AV, 29-Oct-2021.) |
β’ (ClWalksβπΊ) = {β¨π, πβ© β£ (π(WalksβπΊ)π β§ (πβ0) = (πβ(β―βπ)))} | ||
Theorem | isclwlk 29574 | A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(ClWalksβπΊ)π β (πΉ(WalksβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkiswlk 29575 | A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(ClWalksβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | clwlkwlk 29576 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) | ||
Theorem | clwlkswks 29577 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.) |
β’ (ClWalksβπΊ) β (WalksβπΊ) | ||
Theorem | isclwlke 29578* | Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (πΉ(ClWalksβπΊ)π β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | isclwlkupgr 29579* | Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 11-Apr-2021.) (Revised by AV, 28-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β (πΉ(ClWalksβπΊ)π β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | clwlkcomp 29580* | A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ ((πΊ β π β§ π β (π Γ π)) β (π β (ClWalksβπΊ) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | clwlkcompim 29581* | Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ (π β (ClWalksβπΊ) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) | ||
Theorem | upgrclwlkcompim 29582* | Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 2-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ ((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkcompbp 29583 | Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.) |
β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ (π β (ClWalksβπΊ) β (πΉ(WalksβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkl1loop 29584 | A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.) |
β’ ((Fun (iEdgβπΊ) β§ πΉ(ClWalksβπΊ)π β§ (β―βπΉ) = 1) β ((πβ0) = (πβ1) β§ {(πβ0)} β (EdgβπΊ))) | ||
Syntax | ccrcts 29585 | Extend class notation with circuits (in a graph). |
class Circuits | ||
Syntax | ccycls 29586 | Extend class notation with cycles (in a graph). |
class Cycles | ||
Definition | df-crcts 29587* |
Define the set of all circuits (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...". Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of [Bollobas] p. 5.), a circuit is a closed trail without repeated edges. So the circuit 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)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ Circuits = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Definition | df-cycls 29588* |
Define the set of all (simple) cycles (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex." According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of [Bollobas] p. 5. However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ Cycles = (π β V β¦ {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Theorem | crcts 29589* | The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (CircuitsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπ)))} | ||
Theorem | cycls 29590* | The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (CyclesβπΊ) = {β¨π, πβ© β£ (π(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπ)))} | ||
Theorem | iscrct 29591 | Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | iscycl 29592 | Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | crctprop 29593 | The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | cyclprop 29594 | The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | crctisclwlk 29595 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(ClWalksβπΊ)π) | ||
Theorem | crctistrl 29596 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(TrailsβπΊ)π) | ||
Theorem | crctiswlk 29597 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cyclispth 29598 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(PathsβπΊ)π) | ||
Theorem | cycliswlk 29599 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cycliscrct 29600 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(CircuitsβπΊ)π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |