![]() |
Metamath
Proof Explorer Theorem List (p. 300 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 | s2elclwwlknon2 29901 | Sufficient conditions of a doubleton word to represent a closed walk on vertex π of length 2. (Contributed by AV, 11-May-2022.) |
β’ πΆ = (ClWWalksNOnβπΊ) & β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π β π β§ π β π β§ {π, π} β πΈ) β β¨βππββ© β (ππΆ2)) | ||
Theorem | clwwlknon2num 29902 | In a πΎ-regular graph πΊ, there are πΎ closed walks on vertex π of length 2. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.) |
β’ ((πΊ RegUSGraph πΎ β§ π β (VtxβπΊ)) β (β―β(π(ClWWalksNOnβπΊ)2)) = πΎ) | ||
Theorem | clwwlknonwwlknonb 29903 | A word over vertices represents a closed walk of a fixed length π on vertex π iff the word concatenated with π represents a walk of length π on π and π. This theorem would not hold for π = 0 and π = β , see clwwlknwwlksnb 29852. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Word π β§ π β β) β (π β (π(ClWWalksNOnβπΊ)π) β (π ++ β¨βπββ©) β (π(π WWalksNOn πΊ)π))) | ||
Theorem | clwwlknonex2lem1 29904 | Lemma 1 for clwwlknonex2 29906: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for π = 2, i.e., (β―βπ) = 0, because (0..^(((β―βπ) + 2) β 1)) = (0..^((0 + 2) β 1)) = (0..^1) = {0} β {-1, 0} = (β βͺ {-1, 0}) = ((0..^(0 β 1)) βͺ {(0 β 1), 0}) = ((0..^((β―βπ) β 1)) βͺ {((β―βπ) β 1), (β―βπ)}). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.) |
β’ ((π β (β€β₯β3) β§ (β―βπ) = (π β 2)) β (0..^(((β―βπ) + 2) β 1)) = ((0..^((β―βπ) β 1)) βͺ {((β―βπ) β 1), (β―βπ)})) | ||
Theorem | clwwlknonex2lem2 29905* | Lemma 2 for clwwlknonex2 29906: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((((π β π β§ π β π β§ π β (β€β₯β3)) β§ ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = (π β 2) β§ (πβ0) = π)) β§ {π, π} β πΈ) β βπ β ((0..^((β―βπ) β 1)) βͺ {((β―βπ) β 1), (β―βπ)}){(((π ++ β¨βπββ©) ++ β¨βπββ©)βπ), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π + 1))} β πΈ) | ||
Theorem | clwwlknonex2 29906 | Extending a closed walk π on vertex π by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((π β π β§ π β π β§ π β (β€β₯β3)) β§ {π, π} β πΈ β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π ClWWalksN πΊ)) | ||
Theorem | clwwlknonex2e 29907 | Extending a closed walk π on vertex π by an additional edge (forth and back) results in a closed walk on vertex π. (Contributed by AV, 17-Apr-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((π β π β§ π β π β§ π β (β€β₯β3)) β§ {π, π} β πΈ β§ π β (π(ClWWalksNOnβπΊ)(π β 2))) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π(ClWWalksNOnβπΊ)π)) | ||
Theorem | clwwlknondisj 29908* | The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
β’ Disj π₯ β π (π₯(ClWWalksNOnβπΊ)π) | ||
Theorem | clwwlknun 29909* | The set of closed walks of fixed length π in a simple graph πΊ is the union of the closed walks of the fixed length π on each of the vertices of graph πΊ. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (πΊ β USGraph β (π ClWWalksN πΊ) = βͺ π₯ β π (π₯(ClWWalksNOnβπΊ)π)) | ||
Theorem | clwwlkvbij 29910* | There is a bijection between the set of closed walks of a fixed length π on a fixed vertex π represented by walks (as word) and the set of closed walks (as words) of the fixed length π on the fixed vertex π. The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 7-Jul-2022.) (Proof shortened by AV, 2-Nov-2022.) |
β’ ((π β π β§ π β β) β βπ π:{π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) | ||
Theorem | 0ewlk 29911 | The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.) |
β’ ((πΊ β V β§ π β β0*) β β β (πΊ EdgWalks π)) | ||
Theorem | 1ewlk 29912 | A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.) |
β’ ((πΊ β V β§ π β β0* β§ πΌ β dom (iEdgβπΊ)) β β¨βπΌββ© β (πΊ EdgWalks π)) | ||
Theorem | 0wlk 29913 | A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (β (WalksβπΊ)π β π:(0...0)βΆπ)) | ||
Theorem | is0wlk 29914 | A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ ((π = {β¨0, πβ©} β§ π β π) β β (WalksβπΊ)π) | ||
Theorem | 0wlkonlem1 29915 | Lemma 1 for 0wlkon 29917 and 0trlon 29921. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β (π β π β§ π β π)) | ||
Theorem | 0wlkonlem2 29916 | Lemma 2 for 0wlkon 29917 and 0trlon 29921. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β π β (π βpm (0...0))) | ||
Theorem | 0wlkon 29917 | A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β β (π(WalksOnβπΊ)π)π) | ||
Theorem | 0wlkons1 29918 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β π β β (π(WalksOnβπΊ)π)β¨βπββ©) | ||
Theorem | 0trl 29919 | A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (β (TrailsβπΊ)π β π:(0...0)βΆπ)) | ||
Theorem | is0trl 29920 | A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ ((π = {β¨0, πβ©} β§ π β π) β β (TrailsβπΊ)π) | ||
Theorem | 0trlon 29921 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β β (π(TrailsOnβπΊ)π)π) | ||
Theorem | 0pth 29922 | A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (β (PathsβπΊ)π β π:(0...0)βΆπ)) | ||
Theorem | 0spth 29923 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (β (SPathsβπΊ)π β π:(0...0)βΆπ)) | ||
Theorem | 0pthon 29924 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β β (π(PathsOnβπΊ)π)π) | ||
Theorem | 0pthon1 29925 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (π β π β β (π(PathsOnβπΊ)π){β¨0, πβ©}) | ||
Theorem | 0pthonv 29926* | For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.) |
β’ π = (VtxβπΊ) β β’ (π β π β βπβπ π(π(PathsOnβπΊ)π)π) | ||
Theorem | 0clwlk 29927 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (β (ClWalksβπΊ)π β π:(0...0)βΆπ)) | ||
Theorem | 0clwlkv 29928 | Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β π β§ πΉ = β β§ π:{0}βΆ{π}) β πΉ(ClWalksβπΊ)π) | ||
Theorem | 0clwlk0 29929 | There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
β’ (ClWalksββ ) = β | ||
Theorem | 0crct 29930 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΊ β π β (β (CircuitsβπΊ)π β π:(0...0)βΆ(VtxβπΊ))) | ||
Theorem | 0cycl 29931 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΊ β π β (β (CyclesβπΊ)π β π:(0...0)βΆ(VtxβπΊ))) | ||
Theorem | 1pthdlem1 29932 | Lemma 1 for 1pthd 29940. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© β β’ Fun β‘(π βΎ (1..^(β―βπΉ))) | ||
Theorem | 1pthdlem2 29933 | Lemma 2 for 1pthd 29940. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© β β’ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β | ||
Theorem | 1wlkdlem1 29934 | Lemma 1 for 1wlkd 29938. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π:(0...(β―βπΉ))βΆπ) | ||
Theorem | 1wlkdlem2 29935 | Lemma 2 for 1wlkd 29938. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β π β (πΌβπ½)) | ||
Theorem | 1wlkdlem3 29936 | Lemma 3 for 1wlkd 29938. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β πΉ β Word dom πΌ) | ||
Theorem | 1wlkdlem4 29937* | Lemma 4 for 1wlkd 29938. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) | ||
Theorem | 1wlkd 29938 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(WalksβπΊ)π) | ||
Theorem | 1trld 29939 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(TrailsβπΊ)π) | ||
Theorem | 1pthd 29940 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(PathsβπΊ)π) | ||
Theorem | 1pthond 29941 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(π(PathsOnβπΊ)π)π) | ||
Theorem | upgr1wlkdlem1 29942 | Lemma 1 for upgr1wlkd 29944. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) β β’ ((π β§ π = π) β ((iEdgβπΊ)βπ½) = {π}) | ||
Theorem | upgr1wlkdlem2 29943 | Lemma 2 for upgr1wlkd 29944. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) β β’ ((π β§ π β π) β {π, π} β ((iEdgβπΊ)βπ½)) | ||
Theorem | upgr1wlkd 29944 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) & β’ (π β πΊ β UPGraph) β β’ (π β πΉ(WalksβπΊ)π) | ||
Theorem | upgr1trld 29945 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) & β’ (π β πΊ β UPGraph) β β’ (π β πΉ(TrailsβπΊ)π) | ||
Theorem | upgr1pthd 29946 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) & β’ (π β πΊ β UPGraph) β β’ (π β πΉ(PathsβπΊ)π) | ||
Theorem | upgr1pthond 29947 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) & β’ (π β πΊ β UPGraph) β β’ (π β πΉ(π(PathsOnβπΊ)π)π) | ||
Theorem | lppthon 29948 | A loop (which is an edge at index π½) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UHGraph β§ π½ β dom πΌ β§ (πΌβπ½) = {π΄}) β β¨βπ½ββ©(π΄(PathsOnβπΊ)π΄)β¨βπ΄π΄ββ©) | ||
Theorem | lp1cycl 29949 | A loop (which is an edge at index π½) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UHGraph β§ π½ β dom πΌ β§ (πΌβπ½) = {π΄}) β β¨βπ½ββ©(CyclesβπΊ)β¨βπ΄π΄ββ©) | ||
Theorem | 1pthon2v 29950* | For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ (π΄ β π β§ π΅ β π) β§ βπ β πΈ {π΄, π΅} β π) β βπβπ π(π΄(PathsOnβπΊ)π΅)π) | ||
Theorem | 1pthon2ve 29951* | For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Proof shortened by AV, 15-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ (π΄ β π β§ π΅ β π) β§ {π΄, π΅} β πΈ) β βπβπ π(π΄(PathsOnβπΊ)π΅)π) | ||
Theorem | wlk2v2elem1 29952 | Lemma 1 for wlk2v2e 29954: πΉ is a length 2 word of over {0}, the domain of the singleton word πΌ. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
β’ πΌ = β¨β{π, π}ββ© & β’ πΉ = β¨β00ββ© β β’ πΉ β Word dom πΌ | ||
Theorem | wlk2v2elem2 29953* | Lemma 2 for wlk2v2e 29954: The values of πΌ after πΉ are edges between two vertices enumerated by π. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
β’ πΌ = β¨β{π, π}ββ© & β’ πΉ = β¨β00ββ© & β’ π β V & β’ π β V & β’ π = β¨βπππββ© β β’ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} | ||
Theorem | wlk2v2e 29954 | In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that πΊ is a simple graph (without loops) only if π β π. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) |
β’ πΌ = β¨β{π, π}ββ© & β’ πΉ = β¨β00ββ© & β’ π β V & β’ π β V & β’ π = β¨βπππββ© & β’ πΊ = β¨{π, π}, πΌβ© β β’ πΉ(WalksβπΊ)π | ||
Theorem | ntrl2v2e 29955 | A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e 29954, but not a trail. Notice that πΊ is a simple graph (without loops) only if π β π. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ πΌ = β¨β{π, π}ββ© & β’ πΉ = β¨β00ββ© & β’ π β V & β’ π β V & β’ π = β¨βπππββ© & β’ πΊ = β¨{π, π}, πΌβ© β β’ Β¬ πΉ(TrailsβπΊ)π | ||
Theorem | 3wlkdlem1 29956 | Lemma 1 for 3wlkd 29967. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© β β’ (β―βπ) = ((β―βπΉ) + 1) | ||
Theorem | 3wlkdlem2 29957 | Lemma 2 for 3wlkd 29967. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© β β’ (0..^(β―βπΉ)) = {0, 1, 2} | ||
Theorem | 3wlkdlem3 29958 | Lemma 3 for 3wlkd 29967. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) β β’ (π β (((πβ0) = π΄ β§ (πβ1) = π΅) β§ ((πβ2) = πΆ β§ (πβ3) = π·))) | ||
Theorem | 3wlkdlem4 29959* | Lemma 4 for 3wlkd 29967. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) β β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) | ||
Theorem | 3wlkdlem5 29960* | Lemma 5 for 3wlkd 29967. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) β β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | 3pthdlem1 29961* | Lemma 1 for 3pthd 29971. (Contributed by AV, 9-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) β β’ (π β βπ β (0..^(β―βπ))βπ β (1..^(β―βπΉ))(π β π β (πβπ) β (πβπ))) | ||
Theorem | 3wlkdlem6 29962 | Lemma 6 for 3wlkd 29967. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β (π΄ β (πΌβπ½) β§ π΅ β (πΌβπΎ) β§ πΆ β (πΌβπΏ))) | ||
Theorem | 3wlkdlem7 29963 | Lemma 7 for 3wlkd 29967. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β (π½ β V β§ πΎ β V β§ πΏ β V)) | ||
Theorem | 3wlkdlem8 29964 | Lemma 8 for 3wlkd 29967. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β ((πΉβ0) = π½ β§ (πΉβ1) = πΎ β§ (πΉβ2) = πΏ)) | ||
Theorem | 3wlkdlem9 29965 | Lemma 9 for 3wlkd 29967. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β ({π΄, π΅} β (πΌβ(πΉβ0)) β§ {π΅, πΆ} β (πΌβ(πΉβ1)) β§ {πΆ, π·} β (πΌβ(πΉβ2)))) | ||
Theorem | 3wlkdlem10 29966* | Lemma 10 for 3wlkd 29967. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) | ||
Theorem | 3wlkd 29967 | Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(WalksβπΊ)π) | ||
Theorem | 3wlkond 29968 | A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(π΄(WalksOnβπΊ)π·)π) | ||
Theorem | 3trld 29969 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(TrailsβπΊ)π) | ||
Theorem | 3trlond 29970 | A trail of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(π΄(TrailsOnβπΊ)π·)π) | ||
Theorem | 3pthd 29971 | A path of length 3 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(PathsβπΊ)π) | ||
Theorem | 3pthond 29972 | A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(π΄(PathsOnβπΊ)π·)π) | ||
Theorem | 3spthd 29973 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ β π·) β β’ (π β πΉ(SPathsβπΊ)π) | ||
Theorem | 3spthond 29974 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ β π·) β β’ (π β πΉ(π΄(SPathsOnβπΊ)π·)π) | ||
Theorem | 3cycld 29975 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ = π·) β β’ (π β πΉ(CyclesβπΊ)π) | ||
Theorem | 3cyclpd 29976 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ = π·) β β’ (π β (πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | upgr3v3e3cycl 29977* | If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
β’ πΈ = (EdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 3) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) | ||
Theorem | uhgr3cyclexlem 29978 | Lemma for uhgr3cyclex 29979. (Contributed by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((((π΄ β π β§ π΅ β π) β§ π΄ β π΅) β§ ((π½ β dom πΌ β§ {π΅, πΆ} = (πΌβπ½)) β§ (πΎ β dom πΌ β§ {πΆ, π΄} = (πΌβπΎ)))) β π½ β πΎ) | ||
Theorem | uhgr3cyclex 29979* | If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | umgr3cyclex 29980* | If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | umgr3v3e3cycl 29981* | If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β UMGraph β (βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) | ||
Theorem | upgr4cycl4dv4e 29982* | If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 4) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) | ||
Syntax | cconngr 29983 | Extend class notation with connected graphs. |
class ConnGraph | ||
Definition | df-conngr 29984* | Define the class of all connected graphs. A graph is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 29926 and dfconngr1 29985. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ConnGraph = {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} | ||
Theorem | dfconngr1 29985* | Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ConnGraph = {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} | ||
Theorem | isconngr 29986* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) | ||
Theorem | isconngr1 29987* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) | ||
Theorem | cusconngr 29988 | A complete hypergraph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β πΊ β ConnGraph) | ||
Theorem | 0conngr 29989 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ β β ConnGraph | ||
Theorem | 0vconngr 29990 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β πΊ β ConnGraph) | ||
Theorem | 1conngr 29991 | A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph) | ||
Theorem | conngrv2edg 29992* | A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 30092. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ β ran πΌ π β π) | ||
Theorem | vdn0conngrumgrv2 29993 | A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β ((VtxDegβπΊ)βπ) β 0) | ||
According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian." Correspondingly, an Eulerian path is defined as "a trail containing all edges" (see definition in [Bollobas] p. 16) in df-eupth 29995 resp. iseupth 29998. (EulerPathsβπΊ) is the set of all Eulerian paths in graph πΊ, see eupths 29997. An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), or, with other words, a circuit which is an Eulerian path. The function mapping a graph to the set of its Eulerian paths is defined as EulerPaths in df-eupth 29995, whereas there is no explicit definition for Eulerian circuits (yet): The statement "β¨πΉ, πβ© is an Eulerian circuit" is formally expressed by (πΉ(EulerPathsβπΊ)π β§ πΉ(CircuitsβπΊ)π). Each Eulerian path can be made an Eulerian circuit by adding an edge which connects the endpoints of the Eulerian path (see eupth2eucrct 30014). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 30042. An Eulerian path does not have to be a path in the meaning of definition df-pths 29517, because it may traverse some vertices more than once. Therefore, "Eulerian trail" would be a more appropriate name. The main result of this section is (one direction of) Euler's Theorem: "A non-trivial connected graph has an Euler[ian] circuit iff each vertex has even degree." (see part 1 of theorem 12 in [Bollobas] p. 16 and theorem 1.8.1 in [Diestel] p. 22) or, expressed with Eulerian paths: "A connected graph has an Euler[ian] trail from a vertex x to a vertex y (not equal with x) iff x and y are the only vertices of odd degree." (see part 2 of theorem 12 in [Bollobas] p. 17). In eulerpath 30038, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 30039 shows that a pseudograph with an Eulerian circuit has only vertices of even degree. | ||
Syntax | ceupth 29994 | Extend class notation with Eulerian paths. |
class EulerPaths | ||
Definition | df-eupth 29995* | Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ EulerPaths = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ))}) | ||
Theorem | releupth 29996 | The set (EulerPathsβπΊ) of all Eulerian paths on πΊ is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ Rel (EulerPathsβπΊ) | ||
Theorem | eupths 29997* | The Eulerian paths on the graph πΊ. (Contributed by AV, 18-Feb-2021.) (Revised by AV, 29-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (EulerPathsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ π:(0..^(β―βπ))βontoβdom πΌ)} | ||
Theorem | iseupth 29998 | The property "β¨πΉ, πβ© is an Eulerian path on the graph πΊ". An Eulerian path is defined as bijection πΉ from the edges to a set 0...(π β 1) and a function π:(0...π)βΆπ into the vertices such that for each 0 β€ π < π, πΉ(π) is an edge from π(π) to π(π + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ πΉ:(0..^(β―βπΉ))βontoβdom πΌ)) | ||
Theorem | iseupthf1o 29999 | The property "β¨πΉ, πβ© is an Eulerian path on the graph πΊ". An Eulerian path is defined as bijection πΉ from the edges to a set 0...(π β 1) and a function π:(0...π)βΆπ into the vertices such that for each 0 β€ π < π, πΉ(π) is an edge from π(π) to π(π + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(WalksβπΊ)π β§ πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ)) | ||
Theorem | eupthi 30000 | Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(WalksβπΊ)π β§ πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |