![]() |
Metamath
Proof Explorer Theorem List (p. 297 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwlknf1oclwwlkn 29601* | There is a one-to-one onto function between the set of closed walks as words of length π and the set of closed walks of length π in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π΄ = (1st βπ) & β’ π΅ = (2nd βπ) & β’ πΆ = {π€ β (ClWalksβπΊ) β£ (β―β(1st βπ€)) = π} & β’ πΉ = (π β πΆ β¦ (π΅ prefix (β―βπ΄))) β β’ ((πΊ β USPGraph β§ π β β) β πΉ:πΆβ1-1-ontoβ(π ClWWalksN πΊ)) | ||
Theorem | clwlkssizeeq 29602* | The size of the set of closed walks as words of length π corresponds to the size of the set of closed walks of length π in a simple pseudograph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) (Revised by AV, 26-May-2022.) (Proof shortened by AV, 3-Nov-2022.) |
β’ ((πΊ β USPGraph β§ π β β) β (β―β(π ClWWalksN πΊ)) = (β―β{π€ β (ClWalksβπΊ) β£ (β―β(1st βπ€)) = π})) | ||
Theorem | clwlksndivn 29603* | The size of the set of closed walks of prime length π is divisible by π. This corresponds to statement 9 in [Huneke] p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p". (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) |
β’ ((πΊ β FinUSGraph β§ π β β) β π β₯ (β―β{π β (ClWalksβπΊ) β£ (β―β(1st βπ)) = π})) | ||
Syntax | cclwwlknon 29604 | Extend class notation with closed walks (in an undirected graph) anchored at a fixed vertex and of a fixed length as word over the set of vertices. |
class ClWWalksNOn | ||
Definition | df-clwwlknon 29605* | Define the set of all closed walks a graph π, anchored at a fixed vertex π£ (i.e., a walk starting and ending at the fixed vertex π£, also called "a closed walk on vertex π£") and having a fixed length π as words over the set of vertices. Such a word corresponds to the sequence v=p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0)=v as defined in df-clwlks 29292. The set ((π£(ClWWalksNOnβπ)π) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.) |
β’ ClWWalksNOn = (π β V β¦ (π£ β (Vtxβπ), π β β0 β¦ {π€ β (π ClWWalksN π) β£ (π€β0) = π£})) | ||
Theorem | clwwlknonmpo 29606* | (ClWWalksNOnβπΊ) is an operator mapping a vertex π£ and a nonnegative integer π to the set of closed walks on π£ of length π as words over the set of vertices in a graph πΊ. (Contributed by AV, 25-Feb-2022.) (Proof shortened by AV, 2-Mar-2024.) |
β’ (ClWWalksNOnβπΊ) = (π£ β (VtxβπΊ), π β β0 β¦ {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π£}) | ||
Theorem | clwwlknon 29607* | The set of closed walks on vertex π of length π in a graph πΊ as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.) |
β’ (π(ClWWalksNOnβπΊ)π) = {π€ β (π ClWWalksN πΊ) β£ (π€β0) = π} | ||
Theorem | isclwwlknon 29608 | A word over the set of vertices representing a closed walk on vertex π of length π in a graph πΊ. (Contributed by AV, 25-Feb-2022.) (Revised by AV, 24-Mar-2022.) |
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) | ||
Theorem | clwwlk0on0 29609 | There is no word over the set of vertices representing a closed walk on vertex π of length 0 in a graph πΊ. (Contributed by AV, 17-Feb-2022.) (Revised by AV, 25-Feb-2022.) |
β’ (π(ClWWalksNOnβπΊ)0) = β | ||
Theorem | clwwlknon0 29610 | Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022.) |
β’ (Β¬ (π β (VtxβπΊ) β§ π β β) β (π(ClWWalksNOnβπΊ)π) = β ) | ||
Theorem | clwwlknonfin 29611 | In a finite graph πΊ, the set of closed walks on vertex π of length π is also finite. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β Fin β (π(ClWWalksNOnβπΊ)π) β Fin) | ||
Theorem | clwwlknonel 29612* | Characterization of a word over the set of vertices representing a closed walk on vertex π of (nonzero) length π in a graph πΊ. This theorem would not hold for π = 0 if π = π = β . (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β 0 β (π β (π(ClWWalksNOnβπΊ)π) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π β§ (πβ0) = π))) | ||
Theorem | clwwlknonccat 29613 | The concatenation of two words representing closed walks on a vertex π represents a closed walk on vertex π. The resulting walk is a "double loop", starting at vertex π, coming back to π by the first walk, following the second walk and finally coming back to π again. (Contributed by AV, 24-Apr-2022.) |
β’ ((π΄ β (π(ClWWalksNOnβπΊ)π) β§ π΅ β (π(ClWWalksNOnβπΊ)π)) β (π΄ ++ π΅) β (π(ClWWalksNOnβπΊ)(π + π))) | ||
Theorem | clwwlknon1 29614* | The set of closed walks on vertex π of length 1 in a graph πΊ as words over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (ClWWalksNOnβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β π β (ππΆ1) = {π€ β Word π β£ (π€ = β¨βπββ© β§ {π} β πΈ)}) | ||
Theorem | clwwlknon1loop 29615 | If there is a loop at vertex π, the set of (closed) walks on π of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of π. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (ClWWalksNOnβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π β π β§ {π} β πΈ) β (ππΆ1) = {β¨βπββ©}) | ||
Theorem | clwwlknon1nloop 29616 | If there is no loop at vertex π, the set of (closed) walks on π of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (ClWWalksNOnβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ({π} β πΈ β (ππΆ1) = β ) | ||
Theorem | clwwlknon1sn 29617 | The set of (closed) walks on vertex π of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of π iff there is a loop at π. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (ClWWalksNOnβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β π β ((ππΆ1) = {β¨βπββ©} β {π} β πΈ)) | ||
Theorem | clwwlknon1le1 29618 | There is at most one (closed) walk on vertex π of length 1 as word over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
β’ (β―β(π(ClWWalksNOnβπΊ)1)) β€ 1 | ||
Theorem | clwwlknon2 29619* | The set of closed walks on vertex π of length 2 in a graph πΊ as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Revised by AV, 25-Mar-2022.) |
β’ πΆ = (ClWWalksNOnβπΊ) β β’ (ππΆ2) = {π€ β (2 ClWWalksN πΊ) β£ (π€β0) = π} | ||
Theorem | clwwlknon2x 29620* | The set of closed walks on vertex π of length 2 in a graph πΊ as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.) |
β’ πΆ = (ClWWalksNOnβπΊ) & β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (ππΆ2) = {π€ β Word π β£ ((β―βπ€) = 2 β§ {(π€β0), (π€β1)} β πΈ β§ (π€β0) = π)} | ||
Theorem | s2elclwwlknon2 29621 | 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 29622 | 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 29623 | 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 29572. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Word π β§ π β β) β (π β (π(ClWWalksNOnβπΊ)π) β (π ++ β¨βπββ©) β (π(π WWalksNOn πΊ)π))) | ||
Theorem | clwwlknonex2lem1 29624 | Lemma 1 for clwwlknonex2 29626: 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 29625* | Lemma 2 for clwwlknonex2 29626: 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 29626 | 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 29627 | 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 29628* | 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 29629* | 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 29630* | 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 29631 | 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 29632 | 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 29633 | 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 29634 | 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 29635 | Lemma 1 for 0wlkon 29637 and 0trlon 29641. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β (π β π β§ π β π)) | ||
Theorem | 0wlkonlem2 29636 | Lemma 2 for 0wlkon 29637 and 0trlon 29641. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((π:(0...0)βΆπ β§ (πβ0) = π) β π β (π βpm (0...0))) | ||
Theorem | 0wlkon 29637 | 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 29638 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β π β β (π(WalksOnβπΊ)π)β¨βπββ©) | ||
Theorem | 0trl 29639 | 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 29640 | 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 29641 | 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 29642 | 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 29643 | 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 29644 | 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 29645 | 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 29646* | 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 29647 | 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 29648 | 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 29649 | 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 29650 | 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 29651 | 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 29652 | Lemma 1 for 1pthd 29660. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© β β’ Fun β‘(π βΎ (1..^(β―βπΉ))) | ||
Theorem | 1pthdlem2 29653 | Lemma 2 for 1pthd 29660. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© β β’ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β | ||
Theorem | 1wlkdlem1 29654 | Lemma 1 for 1wlkd 29658. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π:(0...(β―βπΉ))βΆπ) | ||
Theorem | 1wlkdlem2 29655 | Lemma 2 for 1wlkd 29658. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β π β (πΌβπ½)) | ||
Theorem | 1wlkdlem3 29656 | Lemma 3 for 1wlkd 29658. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β πΉ β Word dom πΌ) | ||
Theorem | 1wlkdlem4 29657* | Lemma 4 for 1wlkd 29658. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β π) & β’ (π β π β π) & β’ ((π β§ π = π) β (πΌβπ½) = {π}) & β’ ((π β§ π β π) β {π, π} β (πΌβπ½)) β β’ (π β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) | ||
Theorem | 1wlkd 29658 | 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 29659 | 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 29660 | 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 29661 | 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 29662 | Lemma 1 for upgr1wlkd 29664. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) β β’ ((π β§ π = π) β ((iEdgβπΊ)βπ½) = {π}) | ||
Theorem | upgr1wlkdlem2 29663 | Lemma 2 for upgr1wlkd 29664. (Contributed by AV, 22-Jan-2021.) |
β’ π = β¨βππββ© & β’ πΉ = β¨βπ½ββ© & β’ (π β π β (VtxβπΊ)) & β’ (π β π β (VtxβπΊ)) & β’ (π β ((iEdgβπΊ)βπ½) = {π, π}) β β’ ((π β§ π β π) β {π, π} β ((iEdgβπΊ)βπ½)) | ||
Theorem | upgr1wlkd 29664 | 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 29665 | 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 29666 | 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 29667 | 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 29668 | 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 29669 | 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 29670* | 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 29671* | 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 29672 | Lemma 1 for wlk2v2e 29674: πΉ 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 29673* | Lemma 2 for wlk2v2e 29674: 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 29674 | 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 29675 | 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 29674, 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 29676 | Lemma 1 for 3wlkd 29687. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© β β’ (β―βπ) = ((β―βπΉ) + 1) | ||
Theorem | 3wlkdlem2 29677 | Lemma 2 for 3wlkd 29687. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© β β’ (0..^(β―βπΉ)) = {0, 1, 2} | ||
Theorem | 3wlkdlem3 29678 | Lemma 3 for 3wlkd 29687. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) β β’ (π β (((πβ0) = π΄ β§ (πβ1) = π΅) β§ ((πβ2) = πΆ β§ (πβ3) = π·))) | ||
Theorem | 3wlkdlem4 29679* | Lemma 4 for 3wlkd 29687. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) β β’ (π β βπ β (0...(β―βπΉ))(πβπ) β π) | ||
Theorem | 3wlkdlem5 29680* | Lemma 5 for 3wlkd 29687. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) β β’ (π β βπ β (0..^(β―βπΉ))(πβπ) β (πβ(π + 1))) | ||
Theorem | 3pthdlem1 29681* | Lemma 1 for 3pthd 29691. (Contributed by AV, 9-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) β β’ (π β βπ β (0..^(β―βπ))βπ β (1..^(β―βπΉ))(π β π β (πβπ) β (πβπ))) | ||
Theorem | 3wlkdlem6 29682 | Lemma 6 for 3wlkd 29687. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β (π΄ β (πΌβπ½) β§ π΅ β (πΌβπΎ) β§ πΆ β (πΌβπΏ))) | ||
Theorem | 3wlkdlem7 29683 | Lemma 7 for 3wlkd 29687. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β (π½ β V β§ πΎ β V β§ πΏ β V)) | ||
Theorem | 3wlkdlem8 29684 | Lemma 8 for 3wlkd 29687. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β ((πΉβ0) = π½ β§ (πΉβ1) = πΎ β§ (πΉβ2) = πΏ)) | ||
Theorem | 3wlkdlem9 29685 | Lemma 9 for 3wlkd 29687. (Contributed by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β ({π΄, π΅} β (πΌβ(πΉβ0)) β§ {π΅, πΆ} β (πΌβ(πΉβ1)) β§ {πΆ, π·} β (πΌβ(πΉβ2)))) | ||
Theorem | 3wlkdlem10 29686* | Lemma 10 for 3wlkd 29687. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) β β’ (π β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) | ||
Theorem | 3wlkd 29687 | 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 29688 | 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 29689 | 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 29690 | 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 29691 | 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 29692 | 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 29693 | 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 29694 | 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 29695 | 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 29696 | 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 29697* | 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 29698 | Lemma for uhgr3cyclex 29699. (Contributed by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((((π΄ β π β§ π΅ β π) β§ π΄ β π΅) β§ ((π½ β dom πΌ β§ {π΅, πΆ} = (πΌβπ½)) β§ (πΎ β dom πΌ β§ {πΆ, π΄} = (πΌβπΎ)))) β π½ β πΎ) | ||
Theorem | uhgr3cyclex 29699* | 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 29700* | 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) = π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |