![]() |
Metamath
Proof Explorer Theorem List (p. 285 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | numedglnl 28401* | The number of edges incident with a vertex π is the number of edges joining π with other vertices and the number of loops on π in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ (π β Fin β§ πΈ β Fin) β§ π β π) β (Ξ£π£ β (π β {π})(β―β{π β dom πΈ β£ (π β (πΈβπ) β§ π£ β (πΈβπ))}) + (β―β{π β dom πΈ β£ (πΈβπ) = {π}})) = (β―β{π β dom πΈ β£ π β (πΈβπ)})) | ||
Theorem | umgredgne 28402 | An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 28363 resp. umgrnloop 28365. (Contributed by AV, 27-Nov-2020.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π, π} β πΈ) β π β π) | ||
Theorem | umgrnloop2 28403 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) |
β’ (πΊ β UMGraph β {π, π} β (EdgβπΊ)) | ||
Theorem | umgredgnlp 28404* | An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ πΆ β πΈ) β Β¬ βπ£ πΆ = {π£}) | ||
In this section, "simple graph" will always stand for "undirected simple graph (without loops)" and "simple pseudograph" for "undirected simple pseudograph (which could have loops)". | ||
Syntax | cuspgr 28405 | Extend class notation with undirected simple pseudographs (which could have loops). |
class USPGraph | ||
Syntax | cusgr 28406 | Extend class notation with undirected simple graphs (without loops). |
class USGraph | ||
Definition | df-uspgr 28407* | Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 28433) or a special undirected simple hypergraph (see uspgrushgr 28432), consisting of a set π£ (of "vertices") and an injective (one-to-one) function π (representing (indexed) "edges") into subsets of π£ of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ USPGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβ1-1β{π₯ β (π« π£ β {β }) β£ (β―βπ₯) β€ 2}} | ||
Definition | df-usgr 28408* | Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 28435), consisting of a set π£ (of "vertices") and an injective (one-to-one) function π (representing (indexed) "edges") into subsets of π£ of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ USGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβ1-1β{π₯ β (π« π£ β {β }) β£ (β―βπ₯) = 2}} | ||
Theorem | isuspgr 28409* | The property of being a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β USPGraph β πΈ:dom πΈβ1-1β{π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2})) | ||
Theorem | isusgr 28410* | The property of being a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β USGraph β πΈ:dom πΈβ1-1β{π₯ β (π« π β {β }) β£ (β―βπ₯) = 2})) | ||
Theorem | uspgrf 28411* | The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1β{π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | usgrf 28412* | The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β πΈ:dom πΈβ1-1β{π₯ β (π« π β {β }) β£ (β―βπ₯) = 2}) | ||
Theorem | isusgrs 28413* | The property of being a simple graph, simplified version of isusgr 28410. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) (Proof shortened by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β USGraph β πΈ:dom πΈβ1-1β{π₯ β π« π β£ (β―βπ₯) = 2})) | ||
Theorem | usgrfs 28414* | The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 28412. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β πΈ:dom πΈβ1-1β{π₯ β π« π β£ (β―βπ₯) = 2}) | ||
Theorem | usgrfun 28415 | The edge function of a simple graph is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
β’ (πΊ β USGraph β Fun (iEdgβπΊ)) | ||
Theorem | usgredgss 28416* | The set of edges of a simple graph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.) |
β’ (πΊ β USGraph β (EdgβπΊ) β {π₯ β π« (VtxβπΊ) β£ (β―βπ₯) = 2}) | ||
Theorem | edgusgr 28417 | An edge of a simple graph is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 14-Oct-2020.) |
β’ ((πΊ β USGraph β§ πΈ β (EdgβπΊ)) β (πΈ β π« (VtxβπΊ) β§ (β―βπΈ) = 2)) | ||
Theorem | isuspgrop 28418* | The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 25-Nov-2021.) |
β’ ((π β π β§ πΈ β π) β (β¨π, πΈβ© β USPGraph β πΈ:dom πΈβ1-1β{π β (π« π β {β }) β£ (β―βπ) β€ 2})) | ||
Theorem | isusgrop 28419* | The property of being an undirected simple graph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 30-Nov-2020.) |
β’ ((π β π β§ πΈ β π) β (β¨π, πΈβ© β USGraph β πΈ:dom πΈβ1-1β{π β π« π β£ (β―βπ) = 2})) | ||
Theorem | usgrop 28420 | A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020.) (Proof shortened by AV, 30-Nov-2020.) |
β’ (πΊ β USGraph β β¨(VtxβπΊ), (iEdgβπΊ)β© β USGraph) | ||
Theorem | isausgr 28421* | The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} β β’ ((π β π β§ πΈ β π) β (ππΊπΈ β πΈ β {π₯ β π« π β£ (β―βπ₯) = 2})) | ||
Theorem | ausgrusgrb 28422* | The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} β β’ ((π β π β§ πΈ β π) β (ππΊπΈ β β¨π, ( I βΎ πΈ)β© β USGraph)) | ||
Theorem | usgrausgri 28423* | A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} β β’ (π» β USGraph β (Vtxβπ»)πΊ(Edgβπ»)) | ||
Theorem | ausgrumgri 28424* | If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 25-Nov-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} β β’ ((π» β π β§ (Vtxβπ»)πΊ(Edgβπ») β§ Fun (iEdgβπ»)) β π» β UMGraph) | ||
Theorem | ausgrusgri 28425* | The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} & β’ π = {π β£ π:dom πβ1-1βran π} β β’ ((π» β π β§ (Vtxβπ»)πΊ(Edgβπ») β§ (iEdgβπ») β π) β π» β USGraph) | ||
Theorem | usgrausgrb 28426* | The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} & β’ π = {π β£ π:dom πβ1-1βran π} β β’ ((π» β π β§ (iEdgβπ») β π) β ((Vtxβπ»)πΊ(Edgβπ») β π» β USGraph)) | ||
Theorem | usgredgop 28427 | An edge of a simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 15-Oct-2020.) |
β’ ((πΊ β USGraph β§ πΈ = (iEdgβπΊ) β§ π β dom πΈ) β ((πΈβπ) = {π, π} β β¨π, {π, π}β© β πΈ)) | ||
Theorem | usgrf1o 28428 | The edge function of a simple graph is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β πΈ:dom πΈβ1-1-ontoβran πΈ) | ||
Theorem | usgrf1 28429 | The edge function of a simple graph is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) (Revised by AV, 15-Oct-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β πΈ:dom πΈβ1-1βran πΈ) | ||
Theorem | uspgrf1oedg 28430 | The edge function of a simple pseudograph is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ)) | ||
Theorem | usgrss 28431 | An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
β’ πΈ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β (πΈβπ) β π) | ||
Theorem | uspgrushgr 28432 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USPGraph β πΊ β USHGraph) | ||
Theorem | uspgrupgr 28433 | A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USPGraph β πΊ β UPGraph) | ||
Theorem | uspgrupgrushgr 28434 | A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020.) |
β’ (πΊ β USPGraph β (πΊ β UPGraph β§ πΊ β USHGraph)) | ||
Theorem | usgruspgr 28435 | A simple graph is a simple pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USGraph β πΊ β USPGraph) | ||
Theorem | usgrumgr 28436 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
β’ (πΊ β USGraph β πΊ β UMGraph) | ||
Theorem | usgrumgruspgr 28437 | A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020.) |
β’ (πΊ β USGraph β (πΊ β UMGraph β§ πΊ β USPGraph)) | ||
Theorem | usgruspgrb 28438* | A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.) |
β’ (πΊ β USGraph β (πΊ β USPGraph β§ βπ β (EdgβπΊ)(β―βπ) = 2)) | ||
Theorem | usgrupgr 28439 | A simple graph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USGraph β πΊ β UPGraph) | ||
Theorem | usgruhgr 28440 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USGraph β πΊ β UHGraph) | ||
Theorem | usgrislfuspgr 28441* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β USGraph β (πΊ β USPGraph β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)})) | ||
Theorem | uspgrun 28442 | The union π of two simple pseudographs πΊ and π» with the same vertex set π is a pseudograph with the vertex π and the union (πΈ βͺ πΉ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020.) |
β’ (π β πΊ β USPGraph) & β’ (π β π» β USPGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UPGraph) | ||
Theorem | uspgrunop 28443 | The union of two simple pseudographs (with the same vertex set): If β¨π, πΈβ© and β¨π, πΉβ© are simple pseudographs, then β¨π, πΈ βͺ πΉβ© is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
β’ (π β πΊ β USPGraph) & β’ (π β π» β USPGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UPGraph) | ||
Theorem | usgrun 28444 | The union π of two simple graphs πΊ and π» with the same vertex set π is a multigraph (not necessarily a simple graph!) with the vertex π and the union (πΈ βͺ πΉ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) |
β’ (π β πΊ β USGraph) & β’ (π β π» β USGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UMGraph) | ||
Theorem | usgrunop 28445 | The union of two simple graphs (with the same vertex set): If β¨π, πΈβ© and β¨π, πΉβ© are simple graphs, then β¨π, πΈ βͺ πΉβ© is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.) |
β’ (π β πΊ β USGraph) & β’ (π β π» β USGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UMGraph) | ||
Theorem | usgredg2 28446 | The value of the "edge function" of a simple graph is a set containing two elements (the vertices the corresponding edge is connecting). (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β (β―β(πΈβπ)) = 2) | ||
Theorem | usgredg2ALT 28447 | Alternate proof of usgredg2 28446, not using umgredg2 28357. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β (β―β(πΈβπ)) = 2) | ||
Theorem | usgredgprv 28448 | In a simple graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β ((πΈβπ) = {π, π} β (π β π β§ π β π))) | ||
Theorem | usgredgprvALT 28449 | Alternate proof of usgredgprv 28448, using usgredg2 28446 instead of umgredgprv 28364. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 16-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β ((πΈβπ) = {π, π} β (π β π β§ π β π))) | ||
Theorem | usgredgppr 28450 | An edge of a simple graph is a proper pair, i.e. a set containing two different elements (the endvertices of the edge). Analogue of usgredg2 28446. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ πΆ β πΈ) β (β―βπΆ) = 2) | ||
Theorem | usgrpredgv 28451 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 28448. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
β’ πΈ = (EdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β USGraph β§ {π, π} β πΈ) β (π β π β§ π β π)) | ||
Theorem | edgssv2 28452 | An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ πΆ β πΈ) β (πΆ β π β§ (β―βπΆ) = 2)) | ||
Theorem | usgredg 28453* | For each edge in a simple graph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Shortened by AV, 25-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ πΆ β πΈ) β βπ β π βπ β π (π β π β§ πΆ = {π, π})) | ||
Theorem | usgrnloopv 28454 | In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β ((πΈβπ) = {π, π} β π β π)) | ||
Theorem | usgrnloopvALT 28455 | Alternate proof of usgrnloopv 28454, not using umgrnloopv 28363. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β ((πΈβπ) = {π, π} β π β π)) | ||
Theorem | usgrnloop 28456* | In a simple graph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β (βπ₯ β dom πΈ(πΈβπ₯) = {π, π} β π β π)) | ||
Theorem | usgrnloopALT 28457* | Alternate proof of usgrnloop 28456, not using umgrnloop 28365. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β (βπ₯ β dom πΈ(πΈβπ₯) = {π, π} β π β π)) | ||
Theorem | usgrnloop0 28458* | A simple graph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β {π₯ β dom πΈ β£ (πΈβπ₯) = {π}} = β ) | ||
Theorem | usgrnloop0ALT 28459* | Alternate proof of usgrnloop0 28458, not using umgrnloop0 28366. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β {π₯ β dom πΈ β£ (πΈβπ₯) = {π}} = β ) | ||
Theorem | usgredgne 28460 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 28454 resp. usgrnloop 28456. (Contributed by Alexander van der Vekens, 2-Sep-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ {π, π} β πΈ) β π β π) | ||
Theorem | usgrf1oedg 28461 | The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by AV, 18-Oct-2020.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β USGraph β πΌ:dom πΌβ1-1-ontoβπΈ) | ||
Theorem | uhgr2edg 28462* | If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π = (VtxβπΊ) β β’ (((πΊ β UHGraph β§ π΄ β π΅) β§ (π΄ β π β§ π΅ β π β§ π β π) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β βπ₯ β dom πΌβπ¦ β dom πΌ(π₯ β π¦ β§ π β (πΌβπ₯) β§ π β (πΌβπ¦))) | ||
Theorem | umgr2edg 28463* | If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 11-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((πΊ β UMGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β βπ₯ β dom πΌβπ¦ β dom πΌ(π₯ β π¦ β§ π β (πΌβπ₯) β§ π β (πΌβπ¦))) | ||
Theorem | usgr2edg 28464* | If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 11-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β βπ₯ β dom πΌβπ¦ β dom πΌ(π₯ β π¦ β§ π β (πΌβπ₯) β§ π β (πΌβπ¦))) | ||
Theorem | umgr2edg1 28465* | If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 8-Jun-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((πΊ β UMGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β Β¬ β!π₯ β dom πΌ π β (πΌβπ₯)) | ||
Theorem | usgr2edg1 28466* | If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 17-Oct-2020.) (Proof shortened by AV, 8-Jun-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β Β¬ β!π₯ β dom πΌ π β (πΌβπ₯)) | ||
Theorem | umgrvad2edg 28467* | If a vertex is adjacent to two different vertices in a multigraph, there are more than one edges starting at this vertex, analogous to usgr2edg 28464. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.) |
β’ πΈ = (EdgβπΊ) β β’ (((πΊ β UMGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β βπ₯ β πΈ βπ¦ β πΈ (π₯ β π¦ β§ π β π₯ β§ π β π¦)) | ||
Theorem | umgr2edgneu 28468* | If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex, analogous to usgr2edg1 28466. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.) |
β’ πΈ = (EdgβπΊ) β β’ (((πΊ β UMGraph β§ π΄ β π΅) β§ ({π, π΄} β πΈ β§ {π΅, π} β πΈ)) β Β¬ β!π₯ β πΈ π β π₯) | ||
Theorem | usgrsizedg 28469 | In a simple graph, the size of the edge function is the number of the edges of the graph. (Contributed by AV, 4-Jan-2020.) (Revised by AV, 7-Jun-2021.) |
β’ (πΊ β USGraph β (β―β(iEdgβπΊ)) = (β―β(EdgβπΊ))) | ||
Theorem | usgredg3 28470* | The value of the "edge function" of a simple graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ) β βπ₯ β π βπ¦ β π (π₯ β π¦ β§ (πΈβπ) = {π₯, π¦})) | ||
Theorem | usgredg4 28471* | For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 17-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ β§ π β (πΈβπ)) β βπ¦ β π (πΈβπ) = {π, π¦}) | ||
Theorem | usgredgreu 28472* | For a vertex incident to an edge there is exactly one other vertex incident to the edge. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β dom πΈ β§ π β (πΈβπ)) β β!π¦ β π (πΈβπ) = {π, π¦}) | ||
Theorem | usgredg2vtx 28473* | For a vertex incident to an edge there is another vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 5-Dec-2020.) |
β’ ((πΊ β USGraph β§ πΈ β (EdgβπΊ) β§ π β πΈ) β βπ¦ β (VtxβπΊ)πΈ = {π, π¦}) | ||
Theorem | uspgredg2vtxeu 28474* | For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 6-Dec-2020.) |
β’ ((πΊ β USPGraph β§ πΈ β (EdgβπΊ) β§ π β πΈ) β β!π¦ β (VtxβπΊ)πΈ = {π, π¦}) | ||
Theorem | usgredg2vtxeu 28475* | For a vertex incident to an edge there is exactly one other vertex incident to the edge in a simple graph. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.) |
β’ ((πΊ β USGraph β§ πΈ β (EdgβπΊ) β§ π β πΈ) β β!π¦ β (VtxβπΊ)πΈ = {π, π¦}) | ||
Theorem | usgredg2vtxeuALT 28476* | Alternate proof of usgredg2vtxeu 28475, using edgiedgb 28311, the general translation from (iEdgβπΊ) to (EdgβπΊ). (Contributed by AV, 18-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((πΊ β USGraph β§ πΈ β (EdgβπΊ) β§ π β πΈ) β β!π¦ β (VtxβπΊ)πΈ = {π, π¦}) | ||
Theorem | uspgredg2vlem 28477* | Lemma for uspgredg2v 28478. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π΄ = {π β πΈ β£ π β π} β β’ ((πΊ β USPGraph β§ π β π΄) β (β©π§ β π π = {π, π§}) β π) | ||
Theorem | uspgredg2v 28478* | In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π΄ = {π β πΈ β£ π β π} & β’ πΉ = (π¦ β π΄ β¦ (β©π§ β π π¦ = {π, π§})) β β’ ((πΊ β USPGraph β§ π β π) β πΉ:π΄β1-1βπ) | ||
Theorem | usgredg2vlem1 28479* | Lemma 1 for usgredg2v 28481. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π΄ = {π₯ β dom πΈ β£ π β (πΈβπ₯)} β β’ ((πΊ β USGraph β§ π β π΄) β (β©π§ β π (πΈβπ) = {π§, π}) β π) | ||
Theorem | usgredg2vlem2 28480* | Lemma 2 for usgredg2v 28481. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π΄ = {π₯ β dom πΈ β£ π β (πΈβπ₯)} β β’ ((πΊ β USGraph β§ π β π΄) β (πΌ = (β©π§ β π (πΈβπ) = {π§, π}) β (πΈβπ) = {πΌ, π})) | ||
Theorem | usgredg2v 28481* | In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π΄ = {π₯ β dom πΈ β£ π β (πΈβπ₯)} & β’ πΉ = (π¦ β π΄ β¦ (β©π§ β π (πΈβπ¦) = {π§, π})) β β’ ((πΊ β USGraph β§ π β π) β πΉ:π΄β1-1βπ) | ||
Theorem | usgriedgleord 28482* | Alternate version of usgredgleord 28487, not using the notation (EdgβπΊ). In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (β―β{π₯ β dom πΈ β£ π β (πΈβπ₯)}) β€ (β―βπ)) | ||
Theorem | ushgredgedg 28483* | In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) & β’ π΄ = {π β dom πΌ β£ π β (πΌβπ)} & β’ π΅ = {π β πΈ β£ π β π} & β’ πΉ = (π₯ β π΄ β¦ (πΌβπ₯)) β β’ ((πΊ β USHGraph β§ π β π) β πΉ:π΄β1-1-ontoβπ΅) | ||
Theorem | usgredgedg 28484* | In a simple graph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 18-Oct-2020.) (Proof shortened by AV, 11-Dec-2020.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) & β’ π΄ = {π β dom πΌ β£ π β (πΌβπ)} & β’ π΅ = {π β πΈ β£ π β π} & β’ πΉ = (π₯ β π΄ β¦ (πΌβπ₯)) β β’ ((πΊ β USGraph β§ π β π) β πΉ:π΄β1-1-ontoβπ΅) | ||
Theorem | ushgredgedgloop 28485* | In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex π and the set of loops at this vertex π. (Contributed by AV, 11-Dec-2020.) (Revised by AV, 6-Jul-2022.) |
β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ π΄ = {π β dom πΌ β£ (πΌβπ) = {π}} & β’ π΅ = {π β πΈ β£ π = {π}} & β’ πΉ = (π₯ β π΄ β¦ (πΌβπ₯)) β β’ ((πΊ β USHGraph β§ π β π) β πΉ:π΄β1-1-ontoβπ΅) | ||
Theorem | uspgredgleord 28486* | In a simple pseudograph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USPGraph β§ π β π) β (β―β{π β πΈ β£ π β π}) β€ (β―βπ)) | ||
Theorem | usgredgleord 28487* | In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 6-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (β―β{π β πΈ β£ π β π}) β€ (β―βπ)) | ||
Theorem | usgredgleordALT 28488* | Alternate proof for usgredgleord 28487 based on usgriedgleord 28482. In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) (Proof shortened by AV, 5-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ π β π) β (β―β{π β πΈ β£ π β π}) β€ (β―βπ)) | ||
Theorem | usgrstrrepe 28489* | Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a simple graph. Instead of requiring (π β πΊ Struct π), it would be sufficient to require (π β Fun (πΊ β {β })) and (π β πΊ β V). (Contributed by AV, 13-Nov-2021.) (Proof shortened by AV, 16-Nov-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (.efβndx) & β’ (π β πΊ Struct π) & β’ (π β (Baseβndx) β dom πΊ) & β’ (π β πΈ β π) & β’ (π β πΈ:dom πΈβ1-1β{π₯ β π« π β£ (β―βπ₯) = 2}) β β’ (π β (πΊ sSet β¨πΌ, πΈβ©) β USGraph) | ||
Theorem | usgr0e 28490 | The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.) |
β’ (π β πΊ β π) & β’ (π β (iEdgβπΊ) = β ) β β’ (π β πΊ β USGraph) | ||
Theorem | usgr0vb 28491 | The null graph, with no vertices, is a simple graph iff the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 16-Oct-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β (πΊ β USGraph β (iEdgβπΊ) = β )) | ||
Theorem | uhgr0v0e 28492 | The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π = β ) β πΈ = β ) | ||
Theorem | uhgr0vsize0 28493 | The size of a hypergraph with no vertices (the null graph) is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ (β―βπ) = 0) β (β―βπΈ) = 0) | ||
Theorem | uhgr0edgfi 28494 | A graph of order 0 (i.e. with 0 vertices) has a finite set of edges. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 8-Jun-2021.) |
β’ ((πΊ β UHGraph β§ (β―β(VtxβπΊ)) = 0) β (EdgβπΊ) β Fin) | ||
Theorem | usgr0v 28495 | The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β β§ (iEdgβπΊ) = β ) β πΊ β USGraph) | ||
Theorem | uhgr0vusgr 28496 | The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020.) |
β’ ((πΊ β UHGraph β§ (VtxβπΊ) = β ) β πΊ β USGraph) | ||
Theorem | usgr0 28497 | The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.) |
β’ β β USGraph | ||
Theorem | uspgr1e 28498 | A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) β β’ (π β πΊ β USPGraph) | ||
Theorem | usgr1e 28499 | A simple graph with one edge (with additional assumption that π΅ β πΆ since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, πΆ}β©}) & β’ (π β π΅ β πΆ) β β’ (π β πΊ β USGraph) | ||
Theorem | usgr0eop 28500 | The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) |
β’ (π β π β β¨π, β β© β USGraph) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |