Home | Metamath
Proof Explorer Theorem List (p. 261 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | umgrnloopv 26001 | In a multigraph, 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, 11-Dec-2020.) |
iEdg UMGraph | ||
Theorem | umgredgprv 26002 | In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either or could be proper classes ( would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.) |
iEdg Vtx UMGraph | ||
Theorem | umgrnloop 26003* | In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.) |
iEdg UMGraph | ||
Theorem | umgrnloop0 26004* | A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
iEdg UMGraph | ||
Theorem | umgr0e 26005 | The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
iEdg UMGraph | ||
Theorem | upgr0e 26006 | The empty graph, with vertices but no edges, is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.) |
iEdg UPGraph | ||
Theorem | upgr1elem 26007* | Lemma for upgr1e 26008 and uspgr1e 26136. (Contributed by AV, 16-Oct-2020.) |
Theorem | upgr1e 26008 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 26136. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
Vtx iEdg UPGraph | ||
Theorem | upgr0eop 26009 | The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 26138, and therefore also a multigraph ( UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) |
UPGraph | ||
Theorem | upgr1eop 26010 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 26139. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
UPGraph | ||
Theorem | upgr0eopALT 26011 | Alternate proof of upgr0eop 26009, using the general theorem gropeld 25925 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr0eop 26009). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
UPGraph | ||
Theorem | upgr1eopALT 26012 | Alternate proof of upgr1eop 26010, using the general theorem gropeld 25925 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr1eop 26010). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
UPGraph | ||
Theorem | upgrun 26013 | The union of two pseudographs and with the same vertex set is a pseudograph with the vertex and the union of the (indexed) edges. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
UPGraph UPGraph iEdg iEdg Vtx Vtx Vtx iEdg UPGraph | ||
Theorem | upgrunop 26014 | The union of two pseudographs (with the same vertex set): If and are pseudographs, then is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
UPGraph UPGraph iEdg iEdg Vtx Vtx UPGraph | ||
Theorem | umgrun 26015 | The union of two multigraphs and with the same vertex set is a multigraph with the vertex and the union of the (indexed) edges. (Contributed by AV, 25-Nov-2020.) |
UMGraph UMGraph iEdg iEdg Vtx Vtx Vtx iEdg UMGraph | ||
Theorem | umgrunop 26016 | The union of two multigraphs (with the same vertex set): If and are multigraphs, then is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
UMGraph UMGraph iEdg iEdg Vtx Vtx UMGraph | ||
For a hypergraph, the property to be "loop-free" is expressed by with and iEdg. is the set of edges which connect at least two vertices. | ||
Theorem | umgrislfupgrlem 26017 | Lemma for umgrislfupgr 26018 and usgrislfuspgr 26079. (Contributed by AV, 27-Jan-2021.) |
Theorem | umgrislfupgr 26018* | A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.) |
Vtx iEdg UMGraph UPGraph | ||
Theorem | lfgredgge2 26019* | An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.) |
iEdg | ||
Theorem | lfgrnloop 26020* | A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.) |
iEdg | ||
Theorem | uhgredgiedgb 26021* | In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) |
iEdg UHGraph Edg | ||
Theorem | uhgriedg0edg0 26022 | A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 8-Dec-2021.) |
UHGraph Edg iEdg | ||
Theorem | uhgredgn0 26023 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) |
UHGraph Edg Vtx | ||
Theorem | edguhgr 26024 | An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 28-Nov-2020.) |
UHGraph Edg Vtx | ||
Theorem | uhgredgrnv 26025 | An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 4-Jun-2021.) |
UHGraph Edg Vtx | ||
Theorem | uhgredgss 26026 | The set of edges of a hypergraph is a subset of the power set of vertices without the empty set. (Contributed by AV, 29-Nov-2020.) |
UHGraph Edg Vtx | ||
Theorem | upgredgss 26027* | The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020.) |
UPGraph Edg Vtx | ||
Theorem | umgredgss 26028* | The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020.) |
UMGraph Edg Vtx | ||
Theorem | edgupgr 26029 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) |
UPGraph Edg Vtx | ||
Theorem | edgumgr 26030 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) |
UMGraph Edg Vtx | ||
Theorem | uhgrvtxedgiedgb 26031* | In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020.) |
Vtx iEdg Edg UHGraph | ||
Theorem | upgredg 26032* | For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.) (Proof shortened by AV, 26-Nov-2021.) |
Vtx Edg UPGraph | ||
Theorem | umgredg 26033* | For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 25-Nov-2020.) |
Vtx Edg UMGraph | ||
Theorem | upgrpredgv 26034 | An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021.) |
Vtx Edg UPGraph | ||
Theorem | umgrpredgv 26035 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 26002. This theorem does not hold for arbitrary pseudographs: if either or is a proper class, then could still hold ( would be either or , see prprc1 4300 or prprc2 4301, i.e. a loop), but or would not be true. (Contributed by AV, 27-Nov-2020.) |
Vtx Edg UMGraph | ||
Theorem | upgredg2vtx 26036* | For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.) |
Vtx Edg UPGraph | ||
Theorem | upgredgpr 26037 | If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.) |
Vtx Edg UPGraph | ||
Theorem | edglnl 26038* | The edges incident with a vertex are the edges joining with other vertices and the loops on in a pseudograph. (Contributed by AV, 18-Dec-2021.) |
Vtx iEdg UPGraph | ||
Theorem | numedglnl 26039* | 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 | ||
Theorem | umgredgne 26040 | An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 26001 resp. umgrnloop 26003. (Contributed by AV, 27-Nov-2020.) |
Edg UMGraph | ||
Theorem | umgrnloop2 26041 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) |
UMGraph Edg | ||
Theorem | umgredgnlp 26042* | 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 26043 | Extend class notation with undirected simple pseudographs (which could have loops). |
USPGraph | ||
Syntax | cusgr 26044 | Extend class notation with undirected simple graphs (without loops). |
USGraph | ||
Definition | df-uspgr 26045* | Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 26071) or a special undirected simple hypergraph (see uspgrushgr 26070), 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 | ||
Definition | df-usgr 26046* | Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 26073), 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 | ||
Theorem | isuspgr 26047* | 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 | ||
Theorem | isusgr 26048* | 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 | ||
Theorem | uspgrf 26049* | 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 | ||
Theorem | usgrf 26050* | 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 | ||
Theorem | isusgrs 26051* | The property of being a simple graph, simplified version of isusgr 26048. (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 | ||
Theorem | usgrfs 26052* | The edge function of a simple graph is a one-to-one function into unordered pairs of vertices. Simplified version of usgrf 26050. (Contributed by Alexander van der Vekens, 13-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
Vtx iEdg USGraph | ||
Theorem | usgrfun 26053 | 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 iEdg | ||
Theorem | usgredgss 26054* | 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 | ||
Theorem | edgusgr 26055 | 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 | ||
Theorem | isuspgrop 26056* | 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 | ||
Theorem | isusgrop 26057* | 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 | ||
Theorem | usgrop 26058 | 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 26059* | 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.) |
Theorem | ausgrusgrb 26060* | The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017.) (Revised by AV, 14-Oct-2020.) |
USGraph | ||
Theorem | usgrausgri 26061* | A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020.) |
USGraph VtxEdg | ||
Theorem | ausgrumgri 26062* | 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.) |
VtxEdg iEdg UMGraph | ||
Theorem | ausgrusgri 26063* | 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.) |
VtxEdg iEdg USGraph | ||
Theorem | usgrausgrb 26064* | 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.) |
iEdg VtxEdg USGraph | ||
Theorem | usgredgop 26065 | 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 | ||
Theorem | usgrf1o 26066 | 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 | ||
Theorem | usgrf1 26067 | 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 | ||
Theorem | uspgrf1oedg 26068 | 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 Edg | ||
Theorem | usgrss 26069 | 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 | ||
Theorem | uspgrushgr 26070 | A simple pseudograph is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 15-Oct-2020.) |
USPGraph USHGraph | ||
Theorem | uspgrupgr 26071 | 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 26072 | 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 26073 | 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 26074 | A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020.) |
USGraph UMGraph | ||
Theorem | usgrumgruspgr 26075 | 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 26076* | A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020.) |
USGraph USPGraph Edg | ||
Theorem | usgrupgr 26077 | 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 26078 | A simple graph is an undirected hypergraph. (Contributed by AV, 9-Feb-2018.) (Revised by AV, 15-Oct-2020.) |
USGraph UHGraph | ||
Theorem | usgrislfuspgr 26079* | A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.) |
Vtx iEdg USGraph USPGraph | ||
Theorem | uspgrun 26080 | 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 Vtx iEdg UPGraph | ||
Theorem | uspgrunop 26081 | 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 UPGraph | ||
Theorem | usgrun 26082 | 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 Vtx iEdg UMGraph | ||
Theorem | usgrunop 26083 | 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 UMGraph | ||
Theorem | usgredg2 26084 | 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 | ||
Theorem | usgredg2ALT 26085 | Alternate proof of usgredg2 26084, not using umgredg2 25995. (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 | ||
Theorem | usgredgprv 26086 | 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 | ||
Theorem | usgredgprvALT 26087 | Alternate proof of usgredgprv 26086, using usgredg2 26084 instead of umgredgprv 26002. (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 | ||
Theorem | usgredgppr 26088 | 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 26084. (Contributed by Alexander van der Vekens, 11-Aug-2017.) (Revised by AV, 9-Jan-2020.) (Revised by AV, 23-Oct-2020.) |
Edg USGraph | ||
Theorem | usgrpredgv 26089 | An edge of a simple graph always connects two vertices. Analogue of usgredgprv 26086. (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 26090 | 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 | ||
Theorem | usgredg 26091* | 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 26092 | 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 26093 | Alternate proof of usgrnloopv 26092, not using umgrnloopv 26001. (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 26094* | 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 | ||
Theorem | usgrnloopALT 26095* | Alternate proof of usgrnloop 26094, not using umgrnloop 26003. (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 | ||
Theorem | usgrnloop0 26096* | 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 | ||
Theorem | usgrnloop0ALT 26097* | Alternate proof of usgrnloop0 26096, not using umgrnloop0 26004. (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 | ||
Theorem | usgredgne 26098 | An edge of a simple graph always connects two different vertices. Analogue of usgrnloopv 26092 resp. usgrnloop 26094. (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 26099 | The edge function of a simple graph is a 1-1 function onto the set of edges. (Contributed by by AV, 18-Oct-2020.) |
iEdg Edg USGraph | ||
Theorem | uhgr2edg 26100* | 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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |