![]() |
Metamath
Proof Explorer Theorem List (p. 291 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 | vdumgr0 29001 | A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UMGraph β§ π β π β§ (β―βπ) = 1) β ((VtxDegβπΊ)βπ) = 0) | ||
Theorem | vtxdun 29002 | The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π½ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (dom πΌ β© dom π½) = β ) & β’ (π β Fun πΌ) & β’ (π β Fun π½) & β’ (π β π β π) & β’ (π β (iEdgβπ) = (πΌ βͺ π½)) β β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegβπ»)βπ))) | ||
Theorem | vtxdfiun 29003 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π½ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (dom πΌ β© dom π½) = β ) & β’ (π β Fun πΌ) & β’ (π β Fun π½) & β’ (π β π β π) & β’ (π β (iEdgβπ) = (πΌ βͺ π½)) & β’ (π β dom πΌ β Fin) & β’ (π β dom π½ β Fin) β β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπΊ)βπ) + ((VtxDegβπ»)βπ))) | ||
Theorem | vtxduhgrun 29004 | The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π½ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (dom πΌ β© dom π½) = β ) & β’ (π β πΊ β UHGraph) & β’ (π β π» β UHGraph) & β’ (π β π β π) & β’ (π β (iEdgβπ) = (πΌ βͺ π½)) β β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegβπ»)βπ))) | ||
Theorem | vtxduhgrfiun 29005 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π½ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (dom πΌ β© dom π½) = β ) & β’ (π β πΊ β UHGraph) & β’ (π β π» β UHGraph) & β’ (π β π β π) & β’ (π β (iEdgβπ) = (πΌ βͺ π½)) & β’ (π β dom πΌ β Fin) & β’ (π β dom π½ β Fin) β β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπΊ)βπ) + ((VtxDegβπ»)βπ))) | ||
Theorem | vtxdlfgrval 29006* | The value of the vertex degree function for a loop-free graph πΊ. (Contributed by AV, 23-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ & β’ π· = (VtxDegβπΊ) β β’ ((πΌ:π΄βΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β§ π β π) β (π·βπ) = (β―β{π₯ β π΄ β£ π β (πΌβπ₯)})) | ||
Theorem | vtxdumgrval 29007* | The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UMGraph β§ π β π) β (π·βπ) = (β―β{π₯ β π΄ β£ π β (πΌβπ₯)})) | ||
Theorem | vtxdusgrval 29008* | The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (π·βπ) = (β―β{π₯ β π΄ β£ π β (πΌβπ₯)})) | ||
Theorem | vtxd0nedgb 29009* | A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (π β π β ((π·βπ) = 0 β Β¬ βπ β dom πΌ π β (πΌβπ))) | ||
Theorem | vtxdushgrfvedglem 29010* | Lemma for vtxdushgrfvedg 29011 and vtxdusgrfvedg 29012. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USHGraph β§ π β π) β (β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxdushgrfvedg 29011* | The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USHGraph β§ π β π) β (π·βπ) = ((β―β{π β πΈ β£ π β π}) +π (β―β{π β πΈ β£ π = {π}}))) | ||
Theorem | vtxdusgrfvedg 29012* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (π·βπ) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxduhgr0nedg 29013* | If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UHGraph β§ π β π β§ (π·βπ) = 0) β Β¬ βπ£ β π {π, π£} β πΈ) | ||
Theorem | vtxdumgr0nedg 29014* | If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 15-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UMGraph β§ π β π β§ (π·βπ) = 0) β Β¬ βπ£ β π {π, π£} β πΈ) | ||
Theorem | vtxduhgr0edgnel 29015* | A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β UHGraph β§ π β π) β ((π·βπ) = 0 β Β¬ βπ β πΈ π β π)) | ||
Theorem | vtxdusgr0edgnel 29016* | A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β ((π·βπ) = 0 β Β¬ βπ β πΈ π β π)) | ||
Theorem | vtxdusgr0edgnelALT 29017* | Alternate proof of vtxdusgr0edgnel 29016, not based on vtxduhgr0edgnel 29015. A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β ((π·βπ) = 0 β Β¬ βπ β πΈ π β π)) | ||
Theorem | vtxdgfusgrf 29018 | The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β (VtxDegβπΊ):πβΆβ0) | ||
Theorem | vtxdgfusgr 29019* | In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 12-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β βπ£ β π ((VtxDegβπΊ)βπ£) β β0) | ||
Theorem | fusgrn0degnn0 29020* | In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 1-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FinUSGraph β§ π β β ) β βπ£ β π βπ β β0 ((VtxDegβπΊ)βπ£) = π) | ||
Theorem | 1loopgruspgr 29021 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 28770). (Contributed by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β πΊ β USPGraph) | ||
Theorem | 1loopgredg 29022 | The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β (EdgβπΊ) = {{π}}) | ||
Theorem | 1loopgrnb0 29023 | In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β (πΊ NeighbVtx π) = β ) | ||
Theorem | 1loopgrvd2 29024 | 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, 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, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β ((VtxDegβπΊ)βπ) = 2) | ||
Theorem | 1loopgrvd0 29025 | The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) & β’ (π β πΎ β (π β {π})) β β’ (π β ((VtxDegβπΊ)βπΎ) = 0) | ||
Theorem | 1hevtxdg0 29026 | The vertex degree of vertex π· in a graph πΊ with only one hyperedge πΈ is 0 if π· is not incident with the edge πΈ. (Contributed by AV, 2-Mar-2021.) |
β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π· β π) & β’ (π β πΈ β π) & β’ (π β π· β πΈ) β β’ (π β ((VtxDegβπΊ)βπ·) = 0) | ||
Theorem | 1hevtxdg1 29027 | 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 29028 | 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 29029 | 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 29030 | 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 29031 | 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 29032 | 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 29033 | Lemma for p1evtxdeq 29034 and p1evtxdp1 29035. (Contributed by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π) β β’ (π β ((VtxDegβπΉ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegββ¨π, {β¨πΎ, πΈβ©}β©)βπ))) | ||
Theorem | p1evtxdeq 29034 | 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 29035 | 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 29036 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28770). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ (π β π β (VtxβπΊ) = π) | ||
Theorem | uspgrloopvtxel 29037 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28770). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π β π) β π β (VtxβπΊ)) | ||
Theorem | uspgrloopiedg 29038 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28770) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (iEdgβπΊ) = {β¨π΄, {π}β©}) | ||
Theorem | uspgrloopedg 29039 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28770) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (EdgβπΊ) = {{π}}) | ||
Theorem | uspgrloopnb0 29040 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28770), 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 29041 | 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 28770), 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 29042 | 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 29043 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π) β π΄ β (VtxβπΊ)) | ||
Theorem | umgr2v2eiedg 29044 | 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 29045 | 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 29046 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β πΊ β UMGraph) | ||
Theorem | umgr2v2enb1 29047 | 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 29048 | 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 29049 | 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 29040, but degree 2, see uspgrloopvd2 29041. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29047, but also degree 2, see umgr2v2evd2 29048. (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 29050 | 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 29051* | 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 29052* | 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 29053* | 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 29054* | 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 29055* | 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 29056* | 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 29057* | 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 29058* | 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 29059* | 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 29060 | Lemma 1 for vtxdginducedm1 29064: 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 29061* | Lemma 2 for vtxdginducedm1 29064: 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 29062* | Lemma 3 for vtxdginducedm1 29064: 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 29063* | Lemma 4 for vtxdginducedm1 29064. (Contributed by AV, 17-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (π β (π β {π}) β (β―β{π β π½ β£ (πΈβπ) = {π}}) = 0) | ||
Theorem | vtxdginducedm1 29064* | 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 29065* | 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 29066* | Lemma for finsumvtxdg2sstep 29070. (Contributed by AV, 15-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπΈ) = ((β―βπ) + (β―βπ½))) | ||
Theorem | finsumvtxdg2ssteplem2 29067* | Lemma for finsumvtxdg2sstep 29070. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((VtxDegβπΊ)βπ) = ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) | ||
Theorem | finsumvtxdg2ssteplem3 29068* | Lemma for finsumvtxdg2sstep 29070. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―βπ½)) | ||
Theorem | finsumvtxdg2ssteplem4 29069* | Lemma for finsumvtxdg2sstep 29070. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) | ||
Theorem | finsumvtxdg2sstep 29070* | Induction step of finsumvtxdg2size 29071: 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 29071* |
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 29072) 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 29072* | 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 29073* | 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 29074* | 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 29075* | 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 29078 and df-rusgr 29079, 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 29115), because {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0} is not a set (see rgrprcx 29113). It is expected that this function is not defined for every π β β0* (how could this be proven?). | ||
Syntax | crgr 29076 | Extend class notation to include the class of all regular graphs. |
class RegGraph | ||
Syntax | crusgr 29077 | Extend class notation to include the class of all regular simple graphs. |
class RegUSGraph | ||
Definition | df-rgr 29078* | 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 29079* | 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 29080* | 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 29081* | 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 29082 | 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 29083 | 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 29084 | 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 29085 | 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 29086 | A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) | ||
Theorem | isrusgr0 29087* | 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 29088* | 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 29089* | 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 29090* | 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 29091* | 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 29092 | 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 29093 | 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 29094 | A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.) |
β’ ((πΊ β UHGraph β§ (EdgβπΊ) = β ) β πΊ RegGraph 0) | ||
Theorem | uhgr0edg0rgrb 29095 | 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 29096 | 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 29097* | 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 29098* | 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 29099* | 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 29100 | 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 π |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |