![]() |
Metamath
Proof Explorer Theorem List (p. 289 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1hevtxdg1 28801 | The vertex degree of vertex π· in a graph πΊ with only one hyperedge πΈ (not being a loop) is 1 if π· is incident with the edge πΈ. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π· β π) & β’ (π β πΈ β π« π) & β’ (π β π· β πΈ) & β’ (π β 2 β€ (β―βπΈ)) β β’ (π β ((VtxDegβπΊ)βπ·) = 1) | ||
Theorem | 1hegrvtxdg1 28802 | The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β π« π) & β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β {π΅, πΆ} β πΈ) & β’ (π β (VtxβπΊ) = π) β β’ (π β ((VtxDegβπΊ)βπ΅) = 1) | ||
Theorem | 1hegrvtxdg1r 28803 | The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β π« π) & β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β {π΅, πΆ} β πΈ) & β’ (π β (VtxβπΊ) = π) β β’ (π β ((VtxDegβπΊ)βπΆ) = 1) | ||
Theorem | 1egrvtxdg1 28804 | The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β β’ (π β ((VtxDegβπΊ)βπ΅) = 1) | ||
Theorem | 1egrvtxdg1r 28805 | The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β β’ (π β ((VtxDegβπΊ)βπΆ) = 1) | ||
Theorem | 1egrvtxdg0 28806 | The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β π· β π) & β’ (π β πΆ β π·) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, π·}β©}) β β’ (π β ((VtxDegβπΊ)βπΆ) = 0) | ||
Theorem | p1evtxdeqlem 28807 | Lemma for p1evtxdeq 28808 and p1evtxdp1 28809. (Contributed by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π) β β’ (π β ((VtxDegβπΉ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegββ¨π, {β¨πΎ, πΈβ©}β©)βπ))) | ||
Theorem | p1evtxdeq 28808 | If an edge πΈ which does not contain vertex π is added to a graph πΊ (yielding a graph πΉ), the degree of π is the same in both graphs. (Contributed by AV, 2-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π) & β’ (π β π β πΈ) β β’ (π β ((VtxDegβπΉ)βπ) = ((VtxDegβπΊ)βπ)) | ||
Theorem | p1evtxdp1 28809 | If an edge πΈ (not being a loop) which contains vertex π is added to a graph πΊ (yielding a graph πΉ), the degree of π is increased by 1. (Contributed by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π« π) & β’ (π β π β πΈ) & β’ (π β 2 β€ (β―βπΈ)) β β’ (π β ((VtxDegβπΉ)βπ) = (((VtxDegβπΊ)βπ) +π 1)) | ||
Theorem | uspgrloopvtx 28810 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ (π β π β (VtxβπΊ) = π) | ||
Theorem | uspgrloopvtxel 28811 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π β π) β π β (VtxβπΊ)) | ||
Theorem | uspgrloopiedg 28812 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (iEdgβπΊ) = {β¨π΄, {π}β©}) | ||
Theorem | uspgrloopedg 28813 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (EdgβπΊ) = {{π}}) | ||
Theorem | uspgrloopnb0 28814 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π β§ π β π) β (πΊ NeighbVtx π) = β ) | ||
Theorem | uspgrloopvd2 28815 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28544), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π β§ π β π) β ((VtxDegβπΊ)βπ) = 2) | ||
Theorem | umgr2v2evtx 28816 | The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (π β π β (VtxβπΊ) = π) | ||
Theorem | umgr2v2evtxel 28817 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π) β π΄ β (VtxβπΊ)) | ||
Theorem | umgr2v2eiedg 28818 | The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (iEdgβπΊ) = {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}) | ||
Theorem | umgr2v2eedg 28819 | The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π β§ π΅ β π) β (EdgβπΊ) = {{π΄, π΅}}) | ||
Theorem | umgr2v2e 28820 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β πΊ β UMGraph) | ||
Theorem | umgr2v2enb1 28821 | In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β (πΊ NeighbVtx π΄) = {π΅}) | ||
Theorem | umgr2v2evd2 28822 | In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β ((VtxDegβπΊ)βπ΄) = 2) | ||
Theorem | hashnbusgrvd 28823 | In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 28814, but degree 2, see uspgrloopvd2 28815. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 28821, but also degree 2, see umgr2v2evd2 28822. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (β―β(πΊ NeighbVtx π)) = ((VtxDegβπΊ)βπ)) | ||
Theorem | usgruvtxvdb 28824 | In a finite simple graph with n vertices a vertex is universal iff the vertex has degree π β 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FinUSGraph β§ π β π) β (π β (UnivVtxβπΊ) β ((VtxDegβπΊ)βπ) = ((β―βπ) β 1))) | ||
Theorem | vdiscusgrb 28825* | A finite simple graph with n vertices is complete iff every vertex has degree π β 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 22-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β (πΊ β ComplUSGraph β βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1))) | ||
Theorem | vdiscusgr 28826* | In a finite complete simple graph with n vertices every vertex has degree π β 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β (βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1) β πΊ β ComplUSGraph)) | ||
Theorem | vtxdusgradjvtx 28827* | The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018.) (Revised by AV, 23-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β ((VtxDegβπΊ)βπ) = (β―β{π£ β π β£ {π, π£} β πΈ})) | ||
Theorem | usgrvd0nedg 28828* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (((VtxDegβπΊ)βπ) = 0 β Β¬ βπ£ β π {π, π£} β πΈ)) | ||
Theorem | uhgrvd00 28829* | If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β UHGraph β (βπ£ β π ((VtxDegβπΊ)βπ£) = 0 β πΈ = β )) | ||
Theorem | usgrvd00 28830* | If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β USGraph β (βπ£ β π ((VtxDegβπΊ)βπ£) = 0 β πΈ = β )) | ||
Theorem | vdegp1ai 28831* | The induction step for a vertex degree calculation. If the degree of π in the edge set πΈ is π, then adding {π, π} to the edge set, where π β π β π, yields degree π as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ π β π & β’ πΌ = (iEdgβπΊ) & β’ πΌ β Word {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2} & β’ ((VtxDegβπΊ)βπ) = π & β’ (VtxβπΉ) = π & β’ π β π & β’ π β π & β’ π β π & β’ π β π & β’ (iEdgβπΉ) = (πΌ ++ β¨β{π, π}ββ©) β β’ ((VtxDegβπΉ)βπ) = π | ||
Theorem | vdegp1bi 28832* | The induction step for a vertex degree calculation, for example in the KΓΆnigsberg graph. If the degree of π in the edge set πΈ is π, then adding {π, π} to the edge set, where π β π, yields degree π + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ π β π & β’ πΌ = (iEdgβπΊ) & β’ πΌ β Word {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2} & β’ ((VtxDegβπΊ)βπ) = π & β’ (VtxβπΉ) = π & β’ π β π & β’ π β π & β’ (iEdgβπΉ) = (πΌ ++ β¨β{π, π}ββ©) β β’ ((VtxDegβπΉ)βπ) = (π + 1) | ||
Theorem | vdegp1ci 28833* | The induction step for a vertex degree calculation, for example in the KΓΆnigsberg graph. If the degree of π in the edge set πΈ is π, then adding {π, π} to the edge set, where π β π, yields degree π + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ π β π & β’ πΌ = (iEdgβπΊ) & β’ πΌ β Word {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2} & β’ ((VtxDegβπΊ)βπ) = π & β’ (VtxβπΉ) = π & β’ π β π & β’ π β π & β’ (iEdgβπΉ) = (πΌ ++ β¨β{π, π}ββ©) β β’ ((VtxDegβπΉ)βπ) = (π + 1) | ||
Theorem | vtxdginducedm1lem1 28834 | Lemma 1 for vtxdginducedm1 28838: the edge function in the induced subgraph π of a pseudograph πΊ obtained by removing one vertex π. (Contributed by AV, 16-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© β β’ (iEdgβπ) = π | ||
Theorem | vtxdginducedm1lem2 28835* | Lemma 2 for vtxdginducedm1 28838: the domain of the edge function in the induced subgraph π of a pseudograph πΊ obtained by removing one vertex π. (Contributed by AV, 16-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© β β’ dom (iEdgβπ) = πΌ | ||
Theorem | vtxdginducedm1lem3 28836* | Lemma 3 for vtxdginducedm1 28838: an edge in the induced subgraph π of a pseudograph πΊ obtained by removing one vertex π. (Contributed by AV, 16-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© β β’ (π» β πΌ β ((iEdgβπ)βπ») = (πΈβπ»)) | ||
Theorem | vtxdginducedm1lem4 28837* | Lemma 4 for vtxdginducedm1 28838. (Contributed by AV, 17-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (π β (π β {π}) β (β―β{π β π½ β£ (πΈβπ) = {π}}) = 0) | ||
Theorem | vtxdginducedm1 28838* | The degree of a vertex π£ in the induced subgraph π of a pseudograph πΊ obtained by removing one vertex π plus the number of edges joining the vertex π£ and the vertex π is the degree of the vertex π£ in the pseudograph πΊ. (Contributed by AV, 17-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) +π (β―β{π β π½ β£ π£ β (πΈβπ)})) | ||
Theorem | vtxdginducedm1fi 28839* | The degree of a vertex π£ in the induced subgraph π of a pseudograph πΊ of finite size obtained by removing one vertex π plus the number of edges joining the vertex π£ and the vertex π is the degree of the vertex π£ in the pseudograph πΊ. (Contributed by AV, 18-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (πΈ β Fin β βπ£ β (π β {π})((VtxDegβπΊ)βπ£) = (((VtxDegβπ)βπ£) + (β―β{π β π½ β£ π£ β (πΈβπ)}))) | ||
Theorem | finsumvtxdg2ssteplem1 28840* | Lemma for finsumvtxdg2sstep 28844. (Contributed by AV, 15-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπΈ) = ((β―βπ) + (β―βπ½))) | ||
Theorem | finsumvtxdg2ssteplem2 28841* | Lemma for finsumvtxdg2sstep 28844. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((VtxDegβπΊ)βπ) = ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) | ||
Theorem | finsumvtxdg2ssteplem3 28842* | Lemma for finsumvtxdg2sstep 28844. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―βπ½)) | ||
Theorem | finsumvtxdg2ssteplem4 28843* | Lemma for finsumvtxdg2sstep 28844. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) | ||
Theorem | finsumvtxdg2sstep 28844* | Induction step of finsumvtxdg2size 28845: In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((π β Fin β Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β Ξ£π£ β π ((VtxDegβπΊ)βπ£) = (2 Β· (β―βπΈ)))) | ||
Theorem | finsumvtxdg2size 28845* |
The sum of the degrees of all vertices of a finite pseudograph of finite
size is twice the size of the pseudograph. See equation (1) in section
I.1 in [Bollobas] p. 4. Here, the
"proof" is simply the statement
"Since each edge has two endvertices, the sum of the degrees is
exactly
twice the number of edges". The formal proof of this theorem (for
pseudographs) is much more complicated, taking also the used auxiliary
theorems into account. The proof for a (finite) simple graph (see
fusgr1th 28846) would be shorter, but nevertheless still
laborious.
Although this theorem would hold also for infinite pseudographs and
pseudographs of infinite size, the proof of this most general version
(see theorem "sumvtxdg2size" below) would require many more
auxiliary
theorems (e.g., the extension of the sum Ξ£
over an arbitrary
set).
I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β Ξ£π£ β π (π·βπ£) = (2 Β· (β―βπΌ))) | ||
Theorem | fusgr1th 28846* | The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in [Bollobas] p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory). (Contributed by AV, 26-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ β FinUSGraph β Ξ£π£ β π (π·βπ£) = (2 Β· (β―βπΌ))) | ||
Theorem | finsumvtxdgeven 28847* | The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in [Bollobas] p. 4, where it is also called the handshaking lemma. (Contributed by AV, 22-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β 2 β₯ Ξ£π£ β π (π·βπ£)) | ||
Theorem | vtxdgoddnumeven 28848* | The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 22-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UPGraph β§ π β Fin β§ πΌ β Fin) β 2 β₯ (β―β{π£ β π β£ Β¬ 2 β₯ (π·βπ£)})) | ||
Theorem | fusgrvtxdgonume 28849* | The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 27-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ β FinUSGraph β 2 β₯ (β―β{π£ β π β£ Β¬ 2 β₯ (π·βπ£)})) | ||
With df-rgr 28852 and df-rusgr 28853, k-regularity of a (simple) graph is defined as predicate RegGraph resp. RegUSGraph. Instead of defining a predicate, an alternative could have been to define a function that maps an extended nonnegative integer to the class of "graphs" in which every vertex has the extended nonnegative integer as degree: RegGraph = (π β β0* β¦ {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π}). This function, however, would not be defined at least for π = 0 (see rgrx0nd 28889), because {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0} is not a set (see rgrprcx 28887). It is expected that this function is not defined for every π β β0* (how could this be proven?). | ||
Syntax | crgr 28850 | Extend class notation to include the class of all regular graphs. |
class RegGraph | ||
Syntax | crusgr 28851 | Extend class notation to include the class of all regular simple graphs. |
class RegUSGraph | ||
Definition | df-rgr 28852* | Define the "k-regular" predicate, which is true for a "graph" being k-regular: read πΊ RegGraph πΎ as "πΊ is πΎ-regular" or "πΊ is a πΎ-regular graph". Note that πΎ is allowed to be positive infinity (πΎ β β0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ RegGraph = {β¨π, πβ© β£ (π β β0* β§ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π)} | ||
Definition | df-rusgr 28853* | Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read πΊ RegUSGraph πΎ as πΊ is a πΎ-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
β’ RegUSGraph = {β¨π, πβ© β£ (π β USGraph β§ π RegGraph π)} | ||
Theorem | isrgr 28854* | The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β π β§ πΎ β π) β (πΊ RegGraph πΎ β (πΎ β β0* β§ βπ£ β π (π·βπ£) = πΎ))) | ||
Theorem | rgrprop 28855* | The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ RegGraph πΎ β (πΎ β β0* β§ βπ£ β π (π·βπ£) = πΎ)) | ||
Theorem | isrusgr 28856 | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
β’ ((πΊ β π β§ πΎ β π) β (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΊ RegGraph πΎ))) | ||
Theorem | rusgrprop 28857 | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΊ RegGraph πΎ)) | ||
Theorem | rusgrrgr 28858 | A k-regular simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
β’ (πΊ RegUSGraph πΎ β πΊ RegGraph πΎ) | ||
Theorem | rusgrusgr 28859 | A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
β’ (πΊ RegUSGraph πΎ β πΊ β USGraph) | ||
Theorem | finrusgrfusgr 28860 | A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) | ||
Theorem | isrusgr0 28861* | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β π β§ πΎ β π) β (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (π·βπ£) = πΎ))) | ||
Theorem | rusgrprop0 28862* | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (π·βπ£) = πΎ)) | ||
Theorem | usgreqdrusgr 28863* | If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (π·βπ£) = πΎ) β πΊ RegUSGraph πΎ) | ||
Theorem | fusgrregdegfi 28864* | In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 19-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β FinUSGraph β§ π β β ) β (βπ£ β π (π·βπ£) = πΎ β πΎ β β0)) | ||
Theorem | fusgrn0eqdrusgr 28865* | If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β FinUSGraph β§ π β β ) β (βπ£ β π (π·βπ£) = πΎ β πΊ RegUSGraph πΎ)) | ||
Theorem | frusgrnn0 28866 | In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β ) β πΎ β β0) | ||
Theorem | 0edg0rgr 28867 | A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ ((πΊ β π β§ (iEdgβπΊ) = β ) β πΊ RegGraph 0) | ||
Theorem | uhgr0edg0rgr 28868 | A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.) |
β’ ((πΊ β UHGraph β§ (EdgβπΊ) = β ) β πΊ RegGraph 0) | ||
Theorem | uhgr0edg0rgrb 28869 | A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
β’ (πΊ β UHGraph β (πΊ RegGraph 0 β (EdgβπΊ) = β )) | ||
Theorem | usgr0edg0rusgr 28870 | A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 19-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
β’ (πΊ β USGraph β (πΊ RegUSGraph 0 β (EdgβπΊ) = β )) | ||
Theorem | 0vtxrgr 28871* | A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β βπ β β0* πΊ RegGraph π) | ||
Theorem | 0vtxrusgr 28872* | A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β β§ (iEdgβπΊ) = β ) β βπ β β0* πΊ RegUSGraph π) | ||
Theorem | 0uhgrrusgr 28873* | The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ ((πΊ β UHGraph β§ (VtxβπΊ) = β ) β βπ β β0* πΊ RegUSGraph π) | ||
Theorem | 0grrusgr 28874 | The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020.) |
β’ βπ β β0* β RegUSGraph π | ||
Theorem | 0grrgr 28875 | The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.) |
β’ βπ β β0* β RegGraph π | ||
Theorem | cusgrrusgr 28876 | A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β ) β πΊ RegUSGraph ((β―βπ) β 1)) | ||
Theorem | cusgrm1rusgr 28877 | A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for π β β€, then the assumption π β β could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FinUSGraph β§ π β β ) β (πΊ β ComplUSGraph β πΊ RegUSGraph ((β―βπ) β 1))) | ||
Theorem | rusgrpropnb 28878* | The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (β―β(πΊ NeighbVtx π£)) = πΎ)) | ||
Theorem | rusgrpropedg 28879* | The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020.) (Revised by AV, 27-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (β―β{π β (EdgβπΊ) β£ π£ β π}) = πΎ)) | ||
Theorem | rusgrpropadjvtx 28880* | The properties of a k-regular simple graph expressed with adjacent vertices. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 27-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0* β§ βπ£ β π (β―β{π β π β£ {π£, π} β (EdgβπΊ)}) = πΎ)) | ||
Theorem | rusgrnumwrdl2 28881* | In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 6-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ π β π) β (β―β{π€ β Word π β£ ((β―βπ€) = 2 β§ (π€β0) = π β§ {(π€β0), (π€β1)} β (EdgβπΊ))}) = πΎ) | ||
Theorem | rusgr1vtxlem 28882* | Lemma for rusgr1vtx 28883. (Contributed by AV, 27-Dec-2020.) |
β’ (((βπ£ β π (β―βπ΄) = πΎ β§ βπ£ β π π΄ = β ) β§ (π β π β§ (β―βπ) = 1)) β πΎ = 0) | ||
Theorem | rusgr1vtx 28883 | If a k-regular simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 27-Dec-2020.) |
β’ (((β―β(VtxβπΊ)) = 1 β§ πΊ RegUSGraph πΎ) β πΎ = 0) | ||
Theorem | rgrusgrprc 28884* | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
β’ {π β USGraph β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0} β V | ||
Theorem | rusgrprc 28885 | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
β’ {π β£ π RegUSGraph 0} β V | ||
Theorem | rgrprc 28886 | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
β’ {π β£ π RegGraph 0} β V | ||
Theorem | rgrprcx 28887* | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
β’ {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0} β V | ||
Theorem | rgrx0ndm 28888* | 0 is not in the domain of the potentially alternative definition of the sets of k-regular graphs for each extended nonnegative integer k. (Contributed by AV, 28-Dec-2020.) |
β’ π = (π β β0* β¦ {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π}) β β’ 0 β dom π | ||
Theorem | rgrx0nd 28889* | The potentially alternatively defined k-regular graphs is not defined for k=0. (Contributed by AV, 28-Dec-2020.) |
β’ π = (π β β0* β¦ {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = π}) β β’ (π β0) = β | ||
A "walk" in a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see definition of [Bollobas] p. 4, or "A walk (of length k) in a graph is a nonempty alternating sequence v0 e0 v1 e1 ... e(k-1) vk of vertices and edges in G such that ei = { vi , vi+1 } for all i < k.", see definition of [Diestel] p. 10. Formalizing these definitions (mainly by representing the indexed vertices and edges by functions), a walk is represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges (e is a third function enumerating the edges within the graph, not within the walk), and p enumerates the vertices, see df-wlks 28894. Hence a walk (of length n) is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Alternatively, one could define a walk as a function π€:(0...(2 Β· π))βΆ((EdgβπΊ) βͺ (VtxβπΊ)) such that for all 0 β€ π β€ π, (π€β(2 Β· π)) β (VtxβπΊ) and for all 0 β€ π β€ (π β 1), (π€β((2 Β· π) + 1)) β (EdgβπΊ) and {(π€β(2 Β· π)), (π€β((2 Β· π) + 2))} β (π€β((2 Β· π) + 1)). Based on our definition of Walks, the class of all walks, more restrictive constructs are defined: * Trails (df-trls 28987): A "walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5, i.e., f(i) =/= f(j) if i =/= j. * Paths (df-pths 29011): A path is a walk whose vertices except the first and the last vertex are distinct, i.e., p(i) =/= p(j) if i < j, except possibly when i = 0 and j = n. * SPaths (simple paths, df-spths 29012): A simple path "is a walk with distinct vertices.", see Notation of [Bollobas] p. 5, i.e., p(i) =/= p(j) if i =/= j. * ClWalks (closed walks, df-clwlks 29066): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n). * Circuits (df-crcts 29081): "A trail whose endvertices coincide (a closed trail) is called a circuit." (see Definition of [Bollobas] p. 5), i.e., f(i) =/= f(j) if i =/= j and p(0) = p(n). Equivalently, a circuit is a closed walk with distinct edges. * Cycles (df-cycls 29082): A path whose endvertices coincide (a closed path) is called a cycle, i.e., p(i) =/= p(j) if i =/= j, except i = 0 and j = n, and p(0) = p(n). Equivalently, a cycle is a closed walk with distinct vertices. * EulerPaths (Eulerian paths, df-eupth 29489): An Eulerian path is "a trail containing all edges [of the graph]" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Note, however, that an Eulerian path needs not be a path. * Eulerian circuit: 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), i.e., f(i) =/= f(j) if i =/= j, p(0) = p(n) and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Hierarchy of all kinds of walks (apply ssriv 3986 and elopabran 5562 to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk 29069, see clwlkwlk 29070 and clwlkswks 29071): * Trails are walks (trliswlk 28992): (TrailsβπΊ) β (WalksβπΊ) * Paths are trails (pthistrl 29020): (PathsβπΊ) β (TrailsβπΊ) * Simple paths are paths (spthispth 29021): (SPathsβπΊ) β (PathsβπΊ) * Closed walks are walks (clwlkiswlk 29069): (ClWalksβπΊ) β (WalksβπΊ) * Circuits are closed walks (crctisclwlk 29089): (CircuitsβπΊ) β (ClWalksβπΊ) * Circuits are trails (crctistrl 29090): (CircuitsβπΊ) β (TrailsβπΊ) * Cycles are paths (cyclispth 29092): (CyclesβπΊ) β (PathsβπΊ) * Cycles are circuits (cycliscrct 29094): (CyclesβπΊ) β (CircuitsβπΊ) * (Non-trivial) cycles are not simple paths (cyclnspth 29095): (πΉ β β β (πΉ(CyclesβπΊ)π β Β¬ πΉ(SPathsβπΊ)π)) * Eulerian paths are trails (eupthistrl 29502): (EulerPathsβπΊ) β (TrailsβπΊ) 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 14467, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definition df-wwlks 29122 for WWalks, 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 this case, the general definitions of walks and the definition of walks as words are equivalent, see wlkiswwlks 29168. 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). Based on this definition of WWalks, the class of all walks as word, more restrictive constructs are defined analogously to the general definition of a walk: * WWalksN (walks of length N as word, df-wwlksn 29123): n = N * WSPathsN (simple paths of length N as word, df-wspthsn 29125): p(i) =/= p(j) if i =/= j and n = N * ClWWalks (closed walks as word, df-clwwlk 29273): p(0) = p(n) * ClWWalksN (closed walks of length N as word, df-clwwlkn 29316): p(0) = p(n) and n = N Finally, there are a couple of definitions for (special) walks β¨πΉ, πβ© having fixed endpoints π΄ and π΅: * Walks with particular endpoints (df-wlkson 28895): πΉ(π΄(WalksOnβπΊ)π΅)π * Trails with particular endpoints (df-trlson 28988): πΉ(π΄(TrailsOnβπΊ)π΅)π * Paths with particular endpoints (df-pthson 29013): πΉ(π΄(PathsOnβπΊ)π΅)π * Simple paths with particular endpoints (df-spthson 29014): πΉ(π΄(SPathsOnβπΊ)π΅)π * Walks of a fixed length π as words with particular endpoints (df-wwlksnon 29124): (π΄(π WWalksNOn πΊ)π΅) * Simple paths of a fixed length π as words with particular endpoints (df-wspthsnon 29126): (π΄(π WSPathsNOn πΊ)π΅) * Closed Walks of a fixed length π as words anchored at a particular vertex π΄ (df-wwlksnon 29124): (π΄(ClWWalksNOnβπΊ)π) | ||
A "walk" within a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. This definition requires the edges to connect two vertices at most (loops are also allowed: if e(i) is a loop, then x(i-1) = x(i)). For hypergraphs containing hyperedges (i.e. edges connecting more than two vertices), however, a more general definition is needed. Two approaches for a definition applicable for arbitrary hypergraphs are used in the literature: "walks on the vertex level" and "walks on the edge level" (see Aksoy, Joslyn, Marrero, Praggastis, Purvine: "Hypernetwork science via high-order hypergraph walks", June 2020, https://doi.org/10.1140/epjds/s13688-020-00231-0): "walks on the edge level": For a positive integer s, an s-walk of length k between hyperedges f and g is a sequence of hyperedges, f=e(0), e(1), ... , e(k)=g, where for j=1, ... , k, e(j-1) =/= e(j) and e(j-1) and e(j) have at least s vertices in common (according to Aksoy et al.). "walks on the vertex level": For a positive integer s, an s-walk of length k between vertices a and b is a sequence of vertices, a=v(0), v(1), ... , v(k)=b, where for j=1, ... , k, v(j-1) and v(j) are connected by at least s edges (analogous to Aksoy et al.). There are two imperfections for the definition for "walks on the edge level": one is that a walk of length 1 consists of two edges (or a walk of length 0 consists of one edge), whereas a walk of length 1 on the vertex level consists of two vertices and one edge (or a walk of length 0 consists of one vertex and no edge). The other is that edges, especially loops, can be traversed only once (and not repeatedly) because of the condition e(j-1) =/= e(j). The latter is avoided in the definition for EdgWalks, see df-ewlks 28893. To be compatible with the (usual) definition of walks for pseudographs, walks also suitable for arbitrary hypergraphs are defined "on the vertex level" in the following as Walks, see df-wlks 28894, restricting s to 1. wlk1ewlk 28935 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level". | ||
Syntax | cewlks 28890 | Extend class notation with s-walks "on the edge level" (of a hypergraph). |
class EdgWalks | ||
Syntax | cwlks 28891 | Extend class notation with walks (i.e. 1-walks) (of a hypergraph). |
class Walks | ||
Syntax | cwlkson 28892 | Extend class notation with walks between two vertices (within a graph). |
class WalksOn | ||
Definition | df-ewlks 28893* | Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., π = 0 (a 0-walk is an arbitrary sequence of hyperedges) and π = +β (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.) |
β’ EdgWalks = (π β V, π β β0* β¦ {π β£ [(iEdgβπ) / π](π β Word dom π β§ βπ β (1..^(β―βπ))π β€ (β―β((πβ(πβ(π β 1))) β© (πβ(πβπ)))))}) | ||
Definition | df-wlks 28894* |
Define the set of all walks (in a hypergraph). Such walks correspond to
the s-walks "on the vertex level" (with s = 1), and also to
1-walks "on
the edge level" (see wlk1walk 28934) discussed in Aksoy et al. The
predicate πΉ(WalksβπΊ)π can be read as "The pair
β¨πΉ, πβ© represents a walk in a graph
πΊ", see also iswlk 28905.
The condition {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πβπ)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (πβπ) = (πβ(π + 1)) should be allowed only if there is a loop at (πβπ). Otherwise, C would be fulfilled by each edge containing (πβπ). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020.) |
β’ Walks = (π β V β¦ {β¨π, πβ© β£ (π β Word dom (iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(πβπ))))}) | ||
Definition | df-wlkson 28895* | Define the collection of walks with particular endpoints (in a hypergraph). The predicate πΉ(π΄(WalksOnβπΊ)π΅)π can be read as "The pair β¨πΉ, πβ© represents a walk from vertex π΄ to vertex π΅ in a graph πΊ", see also iswlkon 28952. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ WalksOn = (π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {β¨π, πβ© β£ (π(Walksβπ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π)})) | ||
Theorem | ewlksfval 28896* | The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β π β§ π β β0*) β (πΊ EdgWalks π) = {π β£ (π β Word dom πΌ β§ βπ β (1..^(β―βπ))π β€ (β―β((πΌβ(πβ(π β 1))) β© (πΌβ(πβπ)))))}) | ||
Theorem | isewlk 28897* | Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β π β§ π β β0* β§ πΉ β π) β (πΉ β (πΊ EdgWalks π) β (πΉ β Word dom πΌ β§ βπ β (1..^(β―βπΉ))π β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))))) | ||
Theorem | ewlkprop 28898* | Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ β (πΊ EdgWalks π) β ((πΊ β V β§ π β β0*) β§ πΉ β Word dom πΌ β§ βπ β (1..^(β―βπΉ))π β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ)))))) | ||
Theorem | ewlkinedg 28899 | The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ β (πΊ EdgWalks π) β§ πΎ β (1..^(β―βπΉ))) β π β€ (β―β((πΌβ(πΉβ(πΎ β 1))) β© (πΌβ(πΉβπΎ))))) | ||
Theorem | ewlkle 28900 | An s-walk of edges is also a t-walk of edges if π‘ β€ π . (Contributed by AV, 4-Jan-2021.) |
β’ ((πΉ β (πΊ EdgWalks π) β§ π β β0* β§ π β€ π) β πΉ β (πΊ EdgWalks π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |