![]() |
Metamath
Proof Explorer Theorem List (p. 291 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pthontrlon 29001 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β πΉ(π΄(TrailsOnβπΊ)π΅)π) | ||
Theorem | pthonpth 29002 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
β’ (πΉ(PathsβπΊ)π β πΉ((πβ0)(PathsOnβπΊ)(πβ(β―βπΉ)))π) | ||
Theorem | isspthonpth 29003 | 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 29004 | 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 29005 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(PathsOnβπΊ)π΅)π) | ||
Theorem | spthonepeq 29006 | 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 29007 | Lemma 1 for uhgrwkspth 29009. (Contributed by AV, 25-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 1) β Fun β‘πΉ) | ||
Theorem | uhgrwkspthlem2 29008 | Lemma 2 for uhgrwkspth 29009. (Contributed by AV, 25-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ ((β―βπΉ) = 1 β§ π΄ β π΅) β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β Fun β‘π) | ||
Theorem | uhgrwkspth 29009 | 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 29010 | 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 29011 | Lemma 1 for usgr2wlkspth 29013. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘πΉ) | ||
Theorem | usgr2wlkspthlem2 29012 | Lemma 2 for usgr2wlkspth 29013. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
β’ ((πΉ(WalksβπΊ)π β§ (πΊ β USGraph β§ (β―βπΉ) = 2 β§ (πβ0) β (πβ(β―βπΉ)))) β Fun β‘π) | ||
Theorem | usgr2wlkspth 29013 | 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 29014 | 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 29015 | 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 29016 | 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 29017* | Lemma for usgr2pth 29018. (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 29018* | 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 29019* | 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 29020* | Lemma 1 for pthd 29023. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ (π β Fun β‘(π βΎ (1..^π ))) | ||
Theorem | pthdlem2lem 29021* | Lemma for pthdlem2 29022. (Contributed by AV, 10-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ ((π β§ (β―βπ) β β β§ (πΌ = 0 β¨ πΌ = π )) β (πβπΌ) β (π β (1..^π ))) | ||
Theorem | pthdlem2 29022* | Lemma 2 for pthd 29023. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
β’ (π β π β Word V) & β’ π = ((β―βπ) β 1) & β’ (π β βπ β (0..^(β―βπ))βπ β (1..^π )(π β π β (πβπ) β (πβπ))) β β’ (π β ((π β {0, π }) β© (π β (1..^π ))) = β ) | ||
Theorem | pthd 29023* | 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 29024 | Extend class notation with closed walks (of a graph). |
class ClWalks | ||
Definition | df-clwlks 29025* |
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 29380. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
β’ ClWalks = (π β V β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Theorem | clwlks 29026* | 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 29027 | 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 29028 | 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 29029 | 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 29030 | 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 29031* | 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 29032* | 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 29033* | 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 29034* | 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 29035* | 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 29036 | Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.) |
β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ (π β (ClWalksβπΊ) β (πΉ(WalksβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkl1loop 29037 | 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 29038 | Extend class notation with circuits (in a graph). |
class Circuits | ||
Syntax | ccycls 29039 | Extend class notation with cycles (in a graph). |
class Cycles | ||
Definition | df-crcts 29040* |
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 29041* |
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 29042* | 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 29043* | 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 29044 | 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 29045 | 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 29046 | 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 29047 | 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 29048 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(ClWalksβπΊ)π) | ||
Theorem | crctistrl 29049 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(TrailsβπΊ)π) | ||
Theorem | crctiswlk 29050 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cyclispth 29051 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(PathsβπΊ)π) | ||
Theorem | cycliswlk 29052 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cycliscrct 29053 | 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βπΊ)π) | ||
Theorem | cyclnspth 29054 | A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ β β β (πΉ(CyclesβπΊ)π β Β¬ πΉ(SPathsβπΊ)π)) | ||
Theorem | cyclispthon 29055 | A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ((πβ0)(PathsOnβπΊ)(πβ0))π) | ||
Theorem | lfgrn1cycl 29056* | In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β (πΉ(CyclesβπΊ)π β (β―βπΉ) β 1)) | ||
Theorem | usgr2trlncrct 29057 | In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2) β (πΉ(TrailsβπΊ)π β Β¬ πΉ(CircuitsβπΊ)π)) | ||
Theorem | umgrn1cycl 29058 | In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
β’ ((πΊ β UMGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 1) | ||
Theorem | uspgrn2crct 29059 | In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 3-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ ((πΊ β USPGraph β§ πΉ(CircuitsβπΊ)π) β (β―βπΉ) β 2) | ||
Theorem | usgrn2cycl 29060 | In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 4-Feb-2021.) |
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 2) | ||
Theorem | crctcshwlkn0lem1 29061 | Lemma for crctcshwlkn0 29072. (Contributed by AV, 13-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β π΅) + 1) β€ π΄) | ||
Theorem | crctcshwlkn0lem2 29062* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π½ β (0...(π β π))) β (πβπ½) = (πβ(π½ + π))) | ||
Theorem | crctcshwlkn0lem3 29063* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π½ β (((π β π) + 1)...π)) β (πβπ½) = (πβ((π½ + π) β π))) | ||
Theorem | crctcshwlkn0lem4 29064* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β β’ (π β βπ β (0..^(π β π))if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshwlkn0lem5 29065* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β β’ (π β βπ β (((π β π) + 1)..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshwlkn0lem6 29066* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) & β’ (π β (πβπ) = (πβ0)) β β’ ((π β§ π½ = (π β π)) β if-((πβπ½) = (πβ(π½ + 1)), (πΌβ(π»βπ½)) = {(πβπ½)}, {(πβπ½), (πβ(π½ + 1))} β (πΌβ(π»βπ½)))) | ||
Theorem | crctcshwlkn0lem7 29067* | Lemma for crctcshwlkn0 29072. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) & β’ (π β (πβπ) = (πβ0)) β β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshlem1 29068 | Lemma for crctcsh 29075. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) β β’ (π β π β β0) | ||
Theorem | crctcshlem2 29069 | Lemma for crctcsh 29075. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) β β’ (π β (β―βπ») = π) | ||
Theorem | crctcshlem3 29070* | Lemma for crctcsh 29075. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β (πΊ β V β§ π» β V β§ π β V)) | ||
Theorem | crctcshlem4 29071* | Lemma for crctcsh 29075. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π = 0) β (π» = πΉ β§ π = π)) | ||
Theorem | crctcshwlkn0 29072* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a walk β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π β 0) β π»(WalksβπΊ)π) | ||
Theorem | crctcshwlk 29073* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a walk β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(WalksβπΊ)π) | ||
Theorem | crctcshtrl 29074* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a trail β¨π», πβ©. (Contributed by AV, 14-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(TrailsβπΊ)π) | ||
Theorem | crctcsh 29075* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a circuit β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(CircuitsβπΊ)π) | ||
In general, a walk is an alternating sequence of vertices and edges, as defined in df-wlks 28853: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14464, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in Definitions df-wwlks 29081 and df-wwlksn 29082, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). | ||
Syntax | cwwlks 29076 | Extend class notation with walks (in a graph) as word over the set of vertices. |
class WWalks | ||
Syntax | cwwlksn 29077 | Extend class notation with walks (in a graph) of a fixed length as word over the set of vertices. |
class WWalksN | ||
Syntax | cwwlksnon 29078 | Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WWalksNOn | ||
Syntax | cwwspthsn 29079 | Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsN | ||
Syntax | cwwspthsnon 29080 | Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsNOn | ||
Definition | df-wwlks 29081* | Define the set of all 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) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 28853. π€ = β has to be excluded because a walk always consists of at least one vertex, see wlkn0 28875. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ WWalks = (π β V β¦ {π€ β Word (Vtxβπ) β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ))}) | ||
Definition | df-wwlksn 29082* | Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 28853. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ WWalksN = (π β β0, π β V β¦ {π€ β (WWalksβπ) β£ (β―βπ€) = (π + 1)}) | ||
Definition | df-wwlksnon 29083* | Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.) |
β’ WWalksNOn = (π β β0, π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π WWalksN π) β£ ((π€β0) = π β§ (π€βπ) = π)})) | ||
Definition | df-wspthsn 29084* | Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ WSPathsN = (π β β0, π β V β¦ {π€ β (π WWalksN π) β£ βπ π(SPathsβπ)π€}) | ||
Definition | df-wspthsnon 29085* | Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ WSPathsNOn = (π β β0, π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) | ||
Theorem | wwlks 29086* | The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (WWalksβπΊ) = {π€ β Word π β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} | ||
Theorem | iswwlks 29087* | A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (WWalksβπΊ) β (π β β β§ π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ)) | ||
Theorem | wwlksn 29088* | The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ (π β β0 β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) | ||
Theorem | iswwlksn 29089 | A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ (π β β0 β (π β (π WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)))) | ||
Theorem | wwlksnprcl 29090 | Derivation of the length of a word π whose concatenation with a singleton word represents a walk of a fixed length π (a partial reverse closure theorem). (Contributed by AV, 4-Mar-2022.) |
β’ ((π β Word π β§ π β β0) β ((π ++ β¨βπββ©) β (π WWalksN πΊ) β (β―βπ) = π)) | ||
Theorem | iswwlksnx 29091* | Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β β0 β (π β (π WWalksN πΊ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ (β―βπ) = (π + 1)))) | ||
Theorem | wwlkbp 29092 | Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (WWalksβπΊ) β (πΊ β V β§ π β Word π)) | ||
Theorem | wwlknbp 29093 | Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 20-May-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word π)) | ||
Theorem | wwlknp 29094* | Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 9-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (π WWalksN πΊ) β (π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ)) | ||
Theorem | wwlknbp1 29095 | Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β (π β β0 β§ π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1))) | ||
Theorem | wwlknvtx 29096* | The symbols of a word π representing a walk of a fixed length π are vertices. (Contributed by AV, 16-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β βπ β (0...π)(πβπ) β (VtxβπΊ)) | ||
Theorem | wwlknllvtx 29097 | If a word π represents a walk of a fixed length π, then the first and the last symbol of the word is a vertex. (Contributed by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π WWalksN πΊ) β ((πβ0) β π β§ (πβπ) β π)) | ||
Theorem | wwlknlsw 29098 | If a word represents a walk of a fixed length, then the last symbol of the word is the endvertex of the walk. (Contributed by AV, 8-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β (πβπ) = (lastSβπ)) | ||
Theorem | wspthsn 29099* | The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ (π WSPathsN πΊ) = {π€ β (π WWalksN πΊ) β£ βπ π(SPathsβπΊ)π€} | ||
Theorem | iswspthn 29100* | An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ (π β (π WSPathsN πΊ) β (π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |