![]() |
Metamath
Proof Explorer Theorem List (p. 293 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vtxdgfisnn0 29201 | The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ β β’ ((π΄ β Fin β§ π β π) β ((VtxDegβπΊ)βπ) β β0) | ||
Theorem | vtxdgfisf 29202 | The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ β β’ ((πΊ β π β§ π΄ β Fin) β (VtxDegβπΊ):πβΆβ0) | ||
Theorem | vtxdeqd 29203 | Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.) |
β’ (π β πΊ β π) & β’ (π β π» β π) & β’ (π β (Vtxβπ») = (VtxβπΊ)) & β’ (π β (iEdgβπ») = (iEdgβπΊ)) β β’ (π β (VtxDegβπ») = (VtxDegβπΊ)) | ||
Theorem | vtxduhgr0e 29204 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 29200. (Contributed by AV, 15-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π β π β§ πΈ = β ) β ((VtxDegβπΊ)βπ) = 0) | ||
Theorem | vtxdlfuhgr1v 29205* | The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} β β’ ((πΊ β UHGraph β§ (β―βπ) = 1 β§ πΌ:dom πΌβΆπΈ) β (π β π β ((VtxDegβπΊ)βπ) = 0)) | ||
Theorem | vdumgr0 29206 | 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 29207 | 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 29208 | 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 29209 | 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 29210 | 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 29211* | 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 29212* | 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 29213* | 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 29214* | 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 29215* | Lemma for vtxdushgrfvedg 29216 and vtxdusgrfvedg 29217. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USHGraph β§ π β π) β (β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxdushgrfvedg 29216* | 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 29217* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (π·βπ) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxduhgr0nedg 29218* | 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 29219* | 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 29220* | 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 29221* | 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 29222* | Alternate proof of vtxdusgr0edgnel 29221, not based on vtxduhgr0edgnel 29220. 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 29223 | 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 29224* | 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 29225* | 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 29226 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 28975). (Contributed by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β πΊ β USPGraph) | ||
Theorem | 1loopgredg 29227 | 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 29228 | 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 29229 | 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 29230 | 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 29231 | 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 29232 | 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 29233 | 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 29234 | 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 29235 | 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 29236 | 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 29237 | 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 29238 | Lemma for p1evtxdeq 29239 and p1evtxdp1 29240. (Contributed by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π) β β’ (π β ((VtxDegβπΉ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegββ¨π, {β¨πΎ, πΈβ©}β©)βπ))) | ||
Theorem | p1evtxdeq 29239 | 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 29240 | 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 29241 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28975). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ (π β π β (VtxβπΊ) = π) | ||
Theorem | uspgrloopvtxel 29242 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28975). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π β π) β π β (VtxβπΊ)) | ||
Theorem | uspgrloopiedg 29243 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28975) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (iEdgβπΊ) = {β¨π΄, {π}β©}) | ||
Theorem | uspgrloopedg 29244 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28975) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (EdgβπΊ) = {{π}}) | ||
Theorem | uspgrloopnb0 29245 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 28975), 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 29246 | 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 28975), 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 29247 | 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 29248 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π) β π΄ β (VtxβπΊ)) | ||
Theorem | umgr2v2eiedg 29249 | 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 29250 | 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 29251 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β πΊ β UMGraph) | ||
Theorem | umgr2v2enb1 29252 | 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 29253 | 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 29254 | 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 29245, but degree 2, see uspgrloopvd2 29246. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29252, but also degree 2, see umgr2v2evd2 29253. (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 29255 | 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 29256* | 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 29257* | 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 29258* | 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 29259* | 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 29260* | 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 29261* | 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 29262* | 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 29263* | 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 29264* | 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 29265 | Lemma 1 for vtxdginducedm1 29269: 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 29266* | Lemma 2 for vtxdginducedm1 29269: 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 29267* | Lemma 3 for vtxdginducedm1 29269: 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 29268* | Lemma 4 for vtxdginducedm1 29269. (Contributed by AV, 17-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (π β (π β {π}) β (β―β{π β π½ β£ (πΈβπ) = {π}}) = 0) | ||
Theorem | vtxdginducedm1 29269* | 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 29270* | 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 29271* | Lemma for finsumvtxdg2sstep 29275. (Contributed by AV, 15-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπΈ) = ((β―βπ) + (β―βπ½))) | ||
Theorem | finsumvtxdg2ssteplem2 29272* | Lemma for finsumvtxdg2sstep 29275. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((VtxDegβπΊ)βπ) = ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) | ||
Theorem | finsumvtxdg2ssteplem3 29273* | Lemma for finsumvtxdg2sstep 29275. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―βπ½)) | ||
Theorem | finsumvtxdg2ssteplem4 29274* | Lemma for finsumvtxdg2sstep 29275. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ ((((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β§ Ξ£π£ β πΎ ((VtxDegβπ)βπ£) = (2 Β· (β―βπ))) β (Ξ£π£ β (π β {π})((VtxDegβπΊ)βπ£) + ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) = (2 Β· ((β―βπ) + (β―βπ½)))) | ||
Theorem | finsumvtxdg2sstep 29275* | Induction step of finsumvtxdg2size 29276: 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 29276* |
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 29277) 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 29277* | 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 29278* | 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 29279* | 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 29280* | 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 29283 and df-rusgr 29284, 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 29320), because {π β£ βπ£ β (Vtxβπ)((VtxDegβπ)βπ£) = 0} is not a set (see rgrprcx 29318). It is expected that this function is not defined for every π β β0* (how could this be proven?). | ||
Syntax | crgr 29281 | Extend class notation to include the class of all regular graphs. |
class RegGraph | ||
Syntax | crusgr 29282 | Extend class notation to include the class of all regular simple graphs. |
class RegUSGraph | ||
Definition | df-rgr 29283* | 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 29284* | 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 29285* | 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 29286* | 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 29287 | 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 29288 | 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 29289 | 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 29290 | 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 29291 | A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) | ||
Theorem | isrusgr0 29292* | 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 29293* | 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 29294* | 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 29295* | 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 29296* | 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 29297 | 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 29298 | 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 29299 | A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.) |
β’ ((πΊ β UHGraph β§ (EdgβπΊ) = β ) β πΊ RegGraph 0) | ||
Theorem | uhgr0edg0rgrb 29300 | 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βπΊ) = β )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |