Home | Metamath
Proof Explorer Theorem List (p. 280 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isausgr 27901* | 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 27902* | 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 27903* | A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.) |
β’ πΊ = {β¨π£, πβ© β£ π β {π₯ β π« π£ β£ (β―βπ₯) = 2}} β β’ (π» β USGraph β (Vtxβπ»)πΊ(Edgβπ»)) | ||
Theorem | ausgrumgri 27904* | 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 27905* | 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 27906* | 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 27907 | 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 27908 | 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 27909 | 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 27910 | 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 27911 | 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 27912 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USPGraph β πΊ β USHGraph) | ||
Theorem | uspgrupgr 27913 | 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 27914 | 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 27915 | 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 27916 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
β’ (πΊ β USGraph β πΊ β UMGraph) | ||
Theorem | usgrumgruspgr 27917 | 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 27918* | 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 27919 | 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 27920 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
β’ (πΊ β USGraph β πΊ β UHGraph) | ||
Theorem | usgrislfuspgr 27921* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β USGraph β (πΊ β USPGraph β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)})) | ||
Theorem | uspgrun 27922 | 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 27923 | 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 27924 | 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 27925 | 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 27926 | 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 27927 | Alternate proof of usgredg2 27926, not using umgredg2 27837. (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 27928 | 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 27929 | Alternate proof of usgredgprv 27928, using usgredg2 27926 instead of umgredgprv 27844. (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 27930 | 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 27926. (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 27931 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 27928. (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 27932 | 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 27933* | 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 27934 | 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 27935 | Alternate proof of usgrnloopv 27934, not using umgrnloopv 27843. (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 27936* | 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 27937* | Alternate proof of usgrnloop 27936, not using umgrnloop 27845. (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 27938* | 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 27939* | Alternate proof of usgrnloop0 27938, not using umgrnloop0 27846. (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 27940 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 27934 resp. usgrnloop 27936. (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 27941 | 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 27942* | 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 27943* | 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 27944* | 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 27945* | 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 27946* | 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 27947* | 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 27944. (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 27948* | 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 27946. 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 27949 | 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 27950* | 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 27951* | 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 27952* | 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 27953* | 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 27954* | 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 27955* | 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 27956* | Alternate proof of usgredg2vtxeu 27955, using edgiedgb 27791, 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 27957* | Lemma for uspgredg2v 27958. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 6-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π΄ = {π β πΈ β£ π β π} β β’ ((πΊ β USPGraph β§ π β π΄) β (β©π§ β π π = {π, π§}) β π) | ||
Theorem | uspgredg2v 27958* | 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 27959* | Lemma 1 for usgredg2v 27961. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π΄ = {π₯ β dom πΈ β£ π β (πΈβπ₯)} β β’ ((πΊ β USGraph β§ π β π΄) β (β©π§ β π (πΈβπ) = {π§, π}) β π) | ||
Theorem | usgredg2vlem2 27960* | Lemma 2 for usgredg2v 27961. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 18-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π΄ = {π₯ β dom πΈ β£ π β (πΈβπ₯)} β β’ ((πΊ β USGraph β§ π β π΄) β (πΌ = (β©π§ β π (πΈβπ) = {π§, π}) β (πΈβπ) = {πΌ, π})) | ||
Theorem | usgredg2v 27961* | 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 27962* | Alternate version of usgredgleord 27967, 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 27963* | 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 27964* | 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 27965* | 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 27966* | 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 27967* | 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 27968* | Alternate proof for usgredgleord 27967 based on usgriedgleord 27962. 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 27969* | 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 27970 | 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 27971 | 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 27972 | The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π = β ) β πΈ = β ) | ||
Theorem | uhgr0vsize0 27973 | 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 27974 | 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 27975 | The null graph, with no vertices, is a simple graph. (Contributed by AV, 1-Nov-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β β§ (iEdgβπΊ) = β ) β πΊ β USGraph) | ||
Theorem | uhgr0vusgr 27976 | 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 27977 | The null graph represented by an empty set is a simple graph. (Contributed by AV, 16-Oct-2020.) |
β’ β β USGraph | ||
Theorem | uspgr1e 27978 | 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 27979 | 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 27980 | 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) | ||
Theorem | uspgr1eop 27981 | A simple pseudograph with (at least) two vertices and one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) |
β’ (((π β π β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β β¨π, {β¨π΄, {π΅, πΆ}β©}β© β USPGraph) | ||
Theorem | uspgr1ewop 27982 | A simple pseudograph with (at least) two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β β¨π, β¨β{π΄, π΅}ββ©β© β USPGraph) | ||
Theorem | uspgr1v1eop 27983 | A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β β¨π, {β¨π΄, {π΅}β©}β© β USPGraph) | ||
Theorem | usgr1eop 27984 | A simple graph with (at least) two different vertices and one edge. If the two vertices were not different, the edge would be a loop. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 18-Oct-2020.) |
β’ (((π β π β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β (π΅ β πΆ β β¨π, {β¨π΄, {π΅, πΆ}β©}β© β USGraph)) | ||
Theorem | uspgr2v1e2w 27985 | A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
β’ ((π΄ β π β§ π΅ β π) β β¨{π΄, π΅}, β¨β{π΄, π΅}ββ©β© β USPGraph) | ||
Theorem | usgr2v1e2w 27986 | A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
β’ ((π΄ β π β§ π΅ β π β§ π΄ β π΅) β β¨{π΄, π΅}, β¨β{π΄, π΅}ββ©β© β USGraph) | ||
Theorem | edg0usgr 27987 | A class without edges is a simple graph. Since ran πΉ = β does not generally imply Fun πΉ, but Fun (iEdgβπΊ) is required for πΊ to be a simple graph, however, this must be provided as assertion. (Contributed by AV, 18-Oct-2020.) |
β’ ((πΊ β π β§ (EdgβπΊ) = β β§ Fun (iEdgβπΊ)) β πΊ β USGraph) | ||
Theorem | lfuhgr1v0e 27988* | A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} β β’ ((πΊ β UHGraph β§ (β―βπ) = 1 β§ πΌ:dom πΌβΆπΈ) β (EdgβπΊ) = β ) | ||
Theorem | usgr1vr 27989 | A simple graph with one vertex has no edges. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 2-Apr-2021.) |
β’ ((π΄ β π β§ (VtxβπΊ) = {π΄}) β (πΊ β USGraph β (iEdgβπΊ) = β )) | ||
Theorem | usgr1v 27990 | A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = {π΄}) β (πΊ β USGraph β (iEdgβπΊ) = β )) | ||
Theorem | usgr1v0edg 27991 | A class with one (or no) vertex is a simple graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 18-Oct-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = {π΄} β§ Fun (iEdgβπΊ)) β (πΊ β USGraph β (EdgβπΊ) = β )) | ||
Theorem | usgrexmpldifpr 27992 | Lemma for usgrexmpledg 27996: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
β’ (({0, 1} β {1, 2} β§ {0, 1} β {2, 0} β§ {0, 1} β {0, 3}) β§ ({1, 2} β {2, 0} β§ {1, 2} β {0, 3} β§ {2, 0} β {0, 3})) | ||
Theorem | usgrexmplef 27993* | Lemma for usgrexmpl 27997. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© β β’ πΈ:dom πΈβ1-1β{π β π« π β£ (β―βπ) = 2} | ||
Theorem | usgrexmpllem 27994 | Lemma for usgrexmpl 27997. (Contributed by AV, 21-Oct-2020.) |
β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((VtxβπΊ) = π β§ (iEdgβπΊ) = πΈ) | ||
Theorem | usgrexmplvtx 27995 | The vertices 0, 1, 2, 3, 4 of the graph πΊ = β¨π, πΈβ©. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ (VtxβπΊ) = ({0, 1, 2} βͺ {3, 4}) | ||
Theorem | usgrexmpledg 27996 | The edges {0, 1}, {1, 2}, {2, 0}, {0, 3} of the graph πΊ = β¨π, πΈβ©. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ (EdgβπΊ) = ({{0, 1}, {1, 2}} βͺ {{2, 0}, {0, 3}}) | ||
Theorem | usgrexmpl 27997 | πΊ is a simple graph of five vertices 0, 1, 2, 3, 4, with edges {0, 1}, {1, 2}, {2, 0}, {0, 3}. (Contributed by Alexander van der Vekens, 15-Aug-2017.) (Revised by AV, 21-Oct-2020.) |
β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ πΊ β USGraph | ||
Theorem | griedg0prc 27998* | The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.) |
β’ π = {β¨π£, πβ© β£ π:β βΆβ } β β’ π β V | ||
Theorem | griedg0ssusgr 27999* | The class of all simple graphs is a superclass of the class of empty graphs represented as ordered pairs. (Contributed by AV, 27-Dec-2020.) |
β’ π = {β¨π£, πβ© β£ π:β βΆβ } β β’ π β USGraph | ||
Theorem | usgrprc 28000 | The class of simple graphs is a proper class (and therefore, because of prcssprc 5281, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.) |
β’ USGraph β V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |