![]() |
Metamath
Proof Explorer Theorem List (p. 294 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cusgrres 29301* | Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ ((πΊ β ComplUSGraph β§ π β π) β π β ComplUSGraph) | ||
Theorem | cusgrsizeindb0 29302 | Base case of the induction in cusgrsize 29307. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ (β―βπ) = 0) β (β―βπΈ) = ((β―βπ)C2)) | ||
Theorem | cusgrsizeindb1 29303 | Base case of the induction in cusgrsize 29307. The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ (β―βπ) = 1) β (β―βπΈ) = ((β―βπ)C2)) | ||
Theorem | cusgrsizeindslem 29304* | Lemma for cusgrsizeinds 29305. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β π) β (β―β{π β πΈ β£ π β π}) = ((β―βπ) β 1)) | ||
Theorem | cusgrsizeinds 29305* | Part 1 of induction step in cusgrsize 29307. The size of a complete simple graph with π vertices is (π β 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} β β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β π) β (β―βπΈ) = (((β―βπ) β 1) + (β―βπΉ))) | ||
Theorem | cusgrsize2inds 29306* | Induction step in cusgrsize 29307. If the size of the complete graph with π vertices reduced by one vertex is "(π β 1) choose 2", the size of the complete graph with π vertices is "π choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} β β’ (π β β0 β ((πΊ β ComplUSGraph β§ (β―βπ) = π β§ π β π) β ((β―βπΉ) = ((β―β(π β {π}))C2) β (β―βπΈ) = ((β―βπ)C2)))) | ||
Theorem | cusgrsize 29307 | The size of a finite complete simple graph with π vertices (π β β0) is (πC2) ("π choose 2") resp. (((π β 1)βπ) / 2), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β ComplUSGraph β§ π β Fin) β (β―βπΈ) = ((β―βπ)C2)) | ||
Theorem | cusgrfilem1 29308* | Lemma 1 for cusgrfi 29311. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ π = {π₯ β π« π β£ βπ β π (π β π β§ π₯ = {π, π})} β β’ ((πΊ β ComplUSGraph β§ π β π) β π β (EdgβπΊ)) | ||
Theorem | cusgrfilem2 29309* | Lemma 2 for cusgrfi 29311. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ π = {π₯ β π« π β£ βπ β π (π β π β§ π₯ = {π, π})} & β’ πΉ = (π₯ β (π β {π}) β¦ {π₯, π}) β β’ (π β π β πΉ:(π β {π})β1-1-ontoβπ) | ||
Theorem | cusgrfilem3 29310* | Lemma 3 for cusgrfi 29311. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ π = {π₯ β π« π β£ βπ β π (π β π β§ π₯ = {π, π})} & β’ πΉ = (π₯ β (π β {π}) β¦ {π₯, π}) β β’ (π β π β (π β Fin β π β Fin)) | ||
Theorem | cusgrfi 29311 | If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β ComplUSGraph β§ πΈ β Fin) β π β Fin) | ||
Theorem | usgredgsscusgredg 29312 | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (Edgβπ») β β’ ((πΊ β USGraph β§ π» β ComplUSGraph) β πΈ β πΉ) | ||
Theorem | usgrsscusgr 29313* | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (Edgβπ») β β’ ((πΊ β USGraph β§ π» β ComplUSGraph) β βπ β πΈ βπ β πΉ π = π) | ||
Theorem | sizusglecusglem1 29314 | Lemma 1 for sizusglecusg 29316. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (Edgβπ») β β’ ((πΊ β USGraph β§ π» β ComplUSGraph) β ( I βΎ πΈ):πΈβ1-1βπΉ) | ||
Theorem | sizusglecusglem2 29315 | Lemma 2 for sizusglecusg 29316. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (Edgβπ») β β’ ((πΊ β USGraph β§ π» β ComplUSGraph β§ πΉ β Fin) β πΈ β Fin) | ||
Theorem | sizusglecusg 29316 | The size of a simple graph with π vertices is at most the size of a complete simple graph with π vertices (π may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (Edgβπ») β β’ ((πΊ β USGraph β§ π» β ComplUSGraph) β (β―βπΈ) β€ (β―βπΉ)) | ||
Theorem | fusgrmaxsize 29317 | The maximum size of a finite simple graph with π vertices is (((π β 1)βπ) / 2). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FinUSGraph β (β―βπΈ) β€ ((β―βπ)C2)) | ||
Syntax | cvtxdg 29318 | Extend class notation with the vertex degree function. |
class VtxDeg | ||
Definition | df-vtxdg 29319* | Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain π’ "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +π is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
β’ VtxDeg = (π β V β¦ β¦(Vtxβπ) / π£β¦β¦(iEdgβπ) / πβ¦(π’ β π£ β¦ ((β―β{π₯ β dom π β£ π’ β (πβπ₯)}) +π (β―β{π₯ β dom π β£ (πβπ₯) = {π’}})))) | ||
Theorem | vtxdgfval 29320* | The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ β β’ (πΊ β π β (VtxDegβπΊ) = (π’ β π β¦ ((β―β{π₯ β π΄ β£ π’ β (πΌβπ₯)}) +π (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π’}})))) | ||
Theorem | vtxdgval 29321* | The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ β β’ (π β π β ((VtxDegβπΊ)βπ) = ((β―β{π₯ β π΄ β£ π β (πΌβπ₯)}) +π (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π}}))) | ||
Theorem | vtxdgfival 29322* | The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ β β’ ((π΄ β Fin β§ π β π) β ((VtxDegβπΊ)βπ) = ((β―β{π₯ β π΄ β£ π β (πΌβπ₯)}) + (β―β{π₯ β π΄ β£ (πΌβπ₯) = {π}}))) | ||
Theorem | vtxdgop 29323 | The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.) |
β’ (πΊ β π β (VtxDegβπΊ) = ((VtxβπΊ)VtxDeg(iEdgβπΊ))) | ||
Theorem | vtxdgf 29324 | The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (VtxDegβπΊ):πβΆβ0*) | ||
Theorem | vtxdgelxnn0 29325 | The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ (π β π β ((VtxDegβπΊ)βπ) β β0*) | ||
Theorem | vtxdg0v 29326 | The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.) |
β’ π = (VtxβπΊ) β β’ ((πΊ = β β§ π β π) β ((VtxDegβπΊ)βπ) = 0) | ||
Theorem | vtxdg0e 29327 | The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a KΓΆnigsberg graph (see also the induction steps vdegp1ai 29389, vdegp1bi 29390 and vdegp1ci 29391). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((π β π β§ πΌ = β ) β ((VtxDegβπΊ)βπ) = 0) | ||
Theorem | vtxdgfisnn0 29328 | 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 29329 | 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 29330 | 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 29331 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 29327. (Contributed by AV, 15-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π β π β§ πΈ = β ) β ((VtxDegβπΊ)βπ) = 0) | ||
Theorem | vtxdlfuhgr1v 29332* | 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 29333 | 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 29334 | 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 29335 | 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 29336 | 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 29337 | 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 29338* | 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 29339* | 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 29340* | 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 29341* | 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 29342* | Lemma for vtxdushgrfvedg 29343 and vtxdusgrfvedg 29344. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USHGraph β§ π β π) β (β―β{π β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ)}) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxdushgrfvedg 29343* | 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 29344* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (π·βπ) = (β―β{π β πΈ β£ π β π})) | ||
Theorem | vtxduhgr0nedg 29345* | 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 29346* | 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 29347* | 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 29348* | 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 29349* | Alternate proof of vtxdusgr0edgnel 29348, not based on vtxduhgr0edgnel 29347. 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 29350 | 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 29351* | 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 29352* | 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 29353 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 29101). (Contributed by AV, 21-Feb-2021.) |
β’ (π β (VtxβπΊ) = π) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π}β©}) β β’ (π β πΊ β USPGraph) | ||
Theorem | 1loopgredg 29354 | 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 29355 | 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 29356 | 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 29357 | 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 29358 | 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 29359 | 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 29360 | 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 29361 | 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 29362 | 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 29363 | 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 29364 | 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 29365 | Lemma for p1evtxdeq 29366 and p1evtxdp1 29367. (Contributed by AV, 3-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β (VtxβπΉ) = π) & β’ (π β (iEdgβπΉ) = (πΌ βͺ {β¨πΎ, πΈβ©})) & β’ (π β πΎ β π) & β’ (π β πΎ β dom πΌ) & β’ (π β π β π) & β’ (π β πΈ β π) β β’ (π β ((VtxDegβπΉ)βπ) = (((VtxDegβπΊ)βπ) +π ((VtxDegββ¨π, {β¨πΎ, πΈβ©}β©)βπ))) | ||
Theorem | p1evtxdeq 29366 | 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 29367 | 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 29368 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29101). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ (π β π β (VtxβπΊ) = π) | ||
Theorem | uspgrloopvtxel 29369 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29101). (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π β π) β π β (VtxβπΊ)) | ||
Theorem | uspgrloopiedg 29370 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29101) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (iEdgβπΊ) = {β¨π΄, {π}β©}) | ||
Theorem | uspgrloopedg 29371 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29101) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨π΄, {π}β©}β© β β’ ((π β π β§ π΄ β π) β (EdgβπΊ) = {{π}}) | ||
Theorem | uspgrloopnb0 29372 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29101), 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 29373 | 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 29101), 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 29374 | 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 29375 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ ((π β π β§ π΄ β π) β π΄ β (VtxβπΊ)) | ||
Theorem | umgr2v2eiedg 29376 | 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 29377 | 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 29378 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
β’ πΊ = β¨π, {β¨0, {π΄, π΅}β©, β¨1, {π΄, π΅}β©}β© β β’ (((π β π β§ π΄ β π β§ π΅ β π) β§ π΄ β π΅) β πΊ β UMGraph) | ||
Theorem | umgr2v2enb1 29379 | 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 29380 | 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 29381 | 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 29372, but degree 2, see uspgrloopvd2 29373. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29379, but also degree 2, see umgr2v2evd2 29380. (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 29382 | 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 29383* | 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 29384* | 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 29385* | 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 29386* | 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 29387* | 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 29388* | 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 29389* | 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 29390* | 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 29391* | 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 29392 | Lemma 1 for vtxdginducedm1 29396: 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 29393* | Lemma 2 for vtxdginducedm1 29396: 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 29394* | Lemma 3 for vtxdginducedm1 29396: 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 29395* | Lemma 4 for vtxdginducedm1 29396. (Contributed by AV, 17-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (π β (π β {π}) β (β―β{π β π½ β£ (πΈβπ) = {π}}) = 0) | ||
Theorem | vtxdginducedm1 29396* | 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 29397* | 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 29398* | Lemma for finsumvtxdg2sstep 29402. (Contributed by AV, 15-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (β―βπΈ) = ((β―βπ) + (β―βπ½))) | ||
Theorem | finsumvtxdg2ssteplem2 29399* | Lemma for finsumvtxdg2sstep 29402. (Contributed by AV, 12-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β ((VtxDegβπΊ)βπ) = ((β―βπ½) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}}))) | ||
Theorem | finsumvtxdg2ssteplem3 29400* | Lemma for finsumvtxdg2sstep 29402. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΎ = (π β {π}) & β’ πΌ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = (πΈ βΎ πΌ) & β’ π = β¨πΎ, πβ© & β’ π½ = {π β dom πΈ β£ π β (πΈβπ)} β β’ (((πΊ β UPGraph β§ π β π) β§ (π β Fin β§ πΈ β Fin)) β (Ξ£π£ β (π β {π})(β―β{π β π½ β£ π£ β (πΈβπ)}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―βπ½)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |