![]() |
Metamath
Proof Explorer Theorem List (p. 284 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 | iedgval3sn 28301 | Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) |
β’ π΄ β V β β’ (iEdgβ{{{π΄}}}) = {π΄} | ||
Theorem | vtxvalprc 28302 | Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) |
β’ (πΆ β V β (VtxβπΆ) = β ) | ||
Theorem | iedgvalprc 28303 | Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) |
β’ (πΆ β V β (iEdgβπΆ) = β ) | ||
Syntax | cedg 28304 | Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph). |
class Edg | ||
Definition | df-edg 28305 | Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless (e.g., edguhgr 28386). Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
β’ Edg = (π β V β¦ ran (iEdgβπ)) | ||
Theorem | edgval 28306 | The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.) |
β’ (EdgβπΊ) = ran (iEdgβπΊ) | ||
Theorem | iedgedg 28307 | An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.) |
β’ πΈ = (iEdgβπΊ) β β’ ((Fun πΈ β§ πΌ β dom πΈ) β (πΈβπΌ) β (EdgβπΊ)) | ||
Theorem | edgopval 28308 | The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
β’ ((π β π β§ πΈ β π) β (Edgββ¨π, πΈβ©) = ran πΈ) | ||
Theorem | edgov 28309 | The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 28308. The representation ran πΈ for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
β’ ((π β π β§ πΈ β π) β (πEdgπΈ) = ran πΈ) | ||
Theorem | edgstruct 28310 | The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.) |
β’ πΊ = {β¨(Baseβndx), πβ©, β¨(.efβndx), πΈβ©} β β’ ((π β π β§ πΈ β π) β (EdgβπΊ) = ran πΈ) | ||
Theorem | edgiedgb 28311* | A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (Fun πΌ β (πΈ β (EdgβπΊ) β βπ₯ β dom πΌ πΈ = (πΌβπ₯))) | ||
Theorem | edg0iedg0 28312 | There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (Fun πΌ β (πΈ = β β πΌ = β )) | ||
For undirected graphs, we will have the following hierarchy/taxonomy: * Undirected Hypergraph: UHGraph * Undirected loop-free graphs: ULFGraph (not defined formally yet) * Undirected simple Hypergraph: USHGraph => USHGraph β UHGraph (ushgruhgr 28326) * Undirected Pseudograph: UPGraph => UPGraph β UHGraph (upgruhgr 28359) * Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph β UHGraph and ULFHGraph β ULFGraph * Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph β USHGraph and ULFSHGraph β ULFHGraph * Undirected simple Pseudograph: USPGraph => USPGraph β UPGraph (uspgrupgr 28433) and USPGraph β USHGraph (uspgrushgr 28432), see also uspgrupgrushgr 28434 * Undirected Muligraph: UMGraph => UMGraph β UPGraph (umgrupgr 28360) and UMGraph β ULFHGraph (umgrislfupgr 28380) * Undirected simple Graph: USGraph => USGraph β USPGraph (usgruspgr 28435) and USGraph β UMGraph (usgrumgr 28436) and USGraph β ULFSHGraph (usgrislfuspgr 28441) see also usgrumgruspgr 28437 | ||
Syntax | cuhgr 28313 | Extend class notation with undirected hypergraphs. |
class UHGraph | ||
Syntax | cushgr 28314 | Extend class notation with undirected simple hypergraphs. |
class USHGraph | ||
Definition | df-uhgr 28315* | Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set π£ (of "vertices") and a function π (representing indexed "edges") into the power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.) |
β’ UHGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβΆ(π« π£ β {β })} | ||
Definition | df-ushgr 28316* | Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function π is an injective (one-to-one) function into subsets of the set of vertices π£, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by AV, 8-Oct-2020.) |
β’ USHGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβ1-1β(π« π£ β {β })} | ||
Theorem | isuhgr 28317 | The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β UHGraph β πΈ:dom πΈβΆ(π« π β {β }))) | ||
Theorem | isushgr 28318 | The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β USHGraph β πΈ:dom πΈβ1-1β(π« π β {β }))) | ||
Theorem | uhgrf 28319 | The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UHGraph β πΈ:dom πΈβΆ(π« π β {β })) | ||
Theorem | ushgrf 28320 | The edge function of an undirected simple hypergraph is a one-to-one function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USHGraph β πΈ:dom πΈβ1-1β(π« π β {β })) | ||
Theorem | uhgrss 28321 | An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UHGraph β§ πΉ β dom πΈ) β (πΈβπΉ) β π) | ||
Theorem | uhgreq12g 28322 | If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ π = (Vtxβπ») & β’ πΉ = (iEdgβπ») β β’ (((πΊ β π β§ π» β π) β§ (π = π β§ πΈ = πΉ)) β (πΊ β UHGraph β π» β UHGraph)) | ||
Theorem | uhgrfun 28323 | The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UHGraph β Fun πΈ) | ||
Theorem | uhgrn0 28324 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UHGraph β§ πΈ Fn π΄ β§ πΉ β π΄) β (πΈβπΉ) β β ) | ||
Theorem | lpvtx 28325 | The endpoints of a loop (which is an edge at index π½) are two (identical) vertices π΄. (Contributed by AV, 1-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UHGraph β§ π½ β dom πΌ β§ (πΌβπ½) = {π΄}) β π΄ β (VtxβπΊ)) | ||
Theorem | ushgruhgr 28326 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
β’ (πΊ β USHGraph β πΊ β UHGraph) | ||
Theorem | isuhgrop 28327 | The property of being an undirected hypergraph 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, 1-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
β’ ((π β π β§ πΈ β π) β (β¨π, πΈβ© β UHGraph β πΈ:dom πΈβΆ(π« π β {β }))) | ||
Theorem | uhgr0e 28328 | The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
β’ (π β πΊ β π) & β’ (π β (iEdgβπΊ) = β ) β β’ (π β πΊ β UHGraph) | ||
Theorem | uhgr0vb 28329 | The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β (πΊ β UHGraph β (iEdgβπΊ) = β )) | ||
Theorem | uhgr0 28330 | The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.) |
β’ β β UHGraph | ||
Theorem | uhgrun 28331 | The union π of two (undirected) hypergraphs πΊ and π» with the same vertex set π is a hypergraph with the vertex π and the union (πΈ βͺ πΉ) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
β’ (π β πΊ β UHGraph) & β’ (π β π» β UHGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UHGraph) | ||
Theorem | uhgrunop 28332 | The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If β¨π, πΈβ© and β¨π, πΉβ© are hypergraphs, then β¨π, πΈ βͺ πΉβ© is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
β’ (π β πΊ β UHGraph) & β’ (π β π» β UHGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UHGraph) | ||
Theorem | ushgrun 28333 | The union π of two (undirected) simple hypergraphs πΊ and π» with the same vertex set π is a (not necessarily simple) hypergraph with the vertex π and the union (πΈ βͺ πΉ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.) |
β’ (π β πΊ β USHGraph) & β’ (π β π» β USHGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UHGraph) | ||
Theorem | ushgrunop 28334 | The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If β¨π, πΈβ© and β¨π, πΉβ© are simple hypergraphs, then β¨π, πΈ βͺ πΉβ© is a (not necessarily simple) hypergraph - 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.) (Revised by AV, 24-Oct-2021.) |
β’ (π β πΊ β USHGraph) & β’ (π β π» β USHGraph) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = (iEdgβπ») & β’ π = (VtxβπΊ) & β’ (π β (Vtxβπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UHGraph) | ||
Theorem | uhgrstrrepe 28335 | Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a hypergraph. Instead of requiring (π β πΊ Struct π), it would be sufficient to require (π β Fun (πΊ β {β })) and (π β πΊ β V). (Contributed by AV, 18-Jan-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
β’ π = (BaseβπΊ) & β’ πΌ = (.efβndx) & β’ (π β πΊ Struct π) & β’ (π β (Baseβndx) β dom πΊ) & β’ (π β πΈ β π) & β’ (π β πΈ:dom πΈβΆ(π« π β {β })) β β’ (π β (πΊ sSet β¨πΌ, πΈβ©) β UHGraph) | ||
Theorem | incistruhgr 28336* | An incidence structure β¨π, πΏ, πΌβ© "where π is a set whose elements are called points, πΏ is a distinct set whose elements are called lines and πΌ β (π Γ πΏ) is the incidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With π = (Baseβπ) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv) and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β π β§ πΌ β (π Γ πΏ) β§ ran πΌ = πΏ) β ((π = π β§ πΈ = (π β πΏ β¦ {π£ β π β£ π£πΌπ})) β πΊ β UHGraph)) | ||
Syntax | cupgr 28337 | Extend class notation with undirected pseudographs. |
class UPGraph | ||
Syntax | cumgr 28338 | Extend class notation with undirected multigraphs. |
class UMGraph | ||
Definition | df-upgr 28339* | Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set π£ (of "vertices") and a 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. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgr 28340). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) |
β’ UPGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβΆ{π₯ β (π« π£ β {β }) β£ (β―βπ₯) β€ 2}} | ||
Definition | df-umgr 28340* | Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set π£ (of "vertices") and a function π (representing indexed "edges") into subsets of π£ of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." To provide uniform definitions for all kinds of graphs, π₯ β (π« π£ β {β }) is used as restriction of the class abstraction, although π₯ β π« π£ would be sufficient (see prprrab 14433 and isumgrs 28353). (Contributed by AV, 24-Nov-2020.) |
β’ UMGraph = {π β£ [(Vtxβπ) / π£][(iEdgβπ) / π]π:dom πβΆ{π₯ β (π« π£ β {β }) β£ (β―βπ₯) = 2}} | ||
Theorem | isupgr 28341* | The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β UPGraph β πΈ:dom πΈβΆ{π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2})) | ||
Theorem | wrdupgr 28342* | The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β π β§ πΈ β Word π) β (πΊ β UPGraph β πΈ β Word {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2})) | ||
Theorem | upgrf 28343* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 28344 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UPGraph β πΈ:dom πΈβΆ{π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | upgrfn 28344* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΈ Fn π΄) β πΈ:π΄βΆ{π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | upgrss 28345 | An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ β dom πΈ) β (πΈβπΉ) β π) | ||
Theorem | upgrn0 28346 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΈ Fn π΄ β§ πΉ β π΄) β (πΈβπΉ) β β ) | ||
Theorem | upgrle 28347 | An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΈ Fn π΄ β§ πΉ β π΄) β (β―β(πΈβπΉ)) β€ 2) | ||
Theorem | upgrfi 28348 | An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΈ Fn π΄ β§ πΉ β π΄) β (πΈβπΉ) β Fin) | ||
Theorem | upgrex 28349* | An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΈ Fn π΄ β§ πΉ β π΄) β βπ₯ β π βπ¦ β π (πΈβπΉ) = {π₯, π¦}) | ||
Theorem | upgrbi 28350* | Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 28-Feb-2021.) |
β’ π β π & β’ π β π β β’ {π, π} β {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2} | ||
Theorem | upgrop 28351 | A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.) |
β’ (πΊ β UPGraph β β¨(VtxβπΊ), (iEdgβπΊ)β© β UPGraph) | ||
Theorem | isumgr 28352* | The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β UMGraph β πΈ:dom πΈβΆ{π₯ β (π« π β {β }) β£ (β―βπ₯) = 2})) | ||
Theorem | isumgrs 28353* | The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β UMGraph β πΈ:dom πΈβΆ{π₯ β π« π β£ (β―βπ₯) = 2})) | ||
Theorem | wrdumgr 28354* | The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β π β§ πΈ β Word π) β (πΊ β UMGraph β πΈ β Word {π₯ β π« π β£ (β―βπ₯) = 2})) | ||
Theorem | umgrf 28355* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 28356 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UMGraph β πΈ:dom πΈβΆ{π₯ β π« π β£ (β―βπ₯) = 2}) | ||
Theorem | umgrfn 28356* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UMGraph β§ πΈ Fn π΄) β πΈ:π΄βΆ{π₯ β π« π β£ (β―βπ₯) = 2}) | ||
Theorem | umgredg2 28357 | An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β UMGraph β§ π β dom πΈ) β (β―β(πΈβπ)) = 2) | ||
Theorem | umgrbi 28358* | Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.) |
β’ π β π & β’ π β π & β’ π β π β β’ {π, π} β {π₯ β π« π β£ (β―βπ₯) = 2} | ||
Theorem | upgruhgr 28359 | An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.) |
β’ (πΊ β UPGraph β πΊ β UHGraph) | ||
Theorem | umgrupgr 28360 | An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.) |
β’ (πΊ β UMGraph β πΊ β UPGraph) | ||
Theorem | umgruhgr 28361 | An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.) |
β’ (πΊ β UMGraph β πΊ β UHGraph) | ||
Theorem | upgrle2 28362 | An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ π β dom πΌ) β (β―β(πΌβπ)) β€ 2) | ||
Theorem | umgrnloopv 28363 | 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 28364 | 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 β§ π β dom πΈ) β ((πΈβπ) = {π, π} β (π β π β§ π β π))) | ||
Theorem | umgrnloop 28365* | 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 β (βπ₯ β dom πΈ(πΈβπ₯) = {π, π} β π β π)) | ||
Theorem | umgrnloop0 28366* | A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UMGraph β {π₯ β dom πΈ β£ (πΈβπ₯) = {π}} = β ) | ||
Theorem | umgr0e 28367 | 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 28368 | 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 28369* | Lemma for upgr1e 28370 and uspgr1e 28498. (Contributed by AV, 16-Oct-2020.) |
β’ (π β {π΅, πΆ} β π) & β’ (π β π΅ β π) β β’ (π β {{π΅, πΆ}} β {π₯ β (π β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | upgr1e 28370 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 28498. (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 28371 | The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 28500, and therefore also a multigraph (πΊ β UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) |
β’ (π β π β β¨π, β β© β UPGraph) | ||
Theorem | upgr1eop 28372 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 28501. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
β’ (((π β π β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β β¨π, {β¨π΄, {π΅, πΆ}β©}β© β UPGraph) | ||
Theorem | upgr0eopALT 28373 | Alternate proof of upgr0eop 28371, using the general theorem gropeld 28290 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 28371). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β β¨π, β β© β UPGraph) | ||
Theorem | upgr1eopALT 28374 | Alternate proof of upgr1eop 28372, using the general theorem gropeld 28290 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 28372). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (((π β π β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β β¨π, {β¨π΄, {π΅, πΆ}β©}β© β UPGraph) | ||
Theorem | upgrun 28375 | 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βπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UPGraph) | ||
Theorem | upgrunop 28376 | 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βπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UPGraph) | ||
Theorem | umgrun 28377 | 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βπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βͺ πΉ)) β β’ (π β π β UMGraph) | ||
Theorem | umgrunop 28378 | 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βπ») = π) & β’ (π β (dom πΈ β© dom πΉ) = β ) β β’ (π β β¨π, (πΈ βͺ πΉ)β© β UMGraph) | ||
For a hypergraph, the property to be "loop-free" is expressed by πΌ:dom πΌβΆπΈ with πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} and πΌ = (iEdgβπΊ). πΈ is the set of edges which connect at least two vertices. | ||
Theorem | umgrislfupgrlem 28379 | Lemma for umgrislfupgr 28380 and usgrislfuspgr 28441. (Contributed by AV, 27-Jan-2021.) |
β’ ({π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2} β© {π₯ β π« π β£ 2 β€ (β―βπ₯)}) = {π₯ β (π« π β {β }) β£ (β―βπ₯) = 2} | ||
Theorem | umgrislfupgr 28380* | A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UMGraph β (πΊ β UPGraph β§ πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)})) | ||
Theorem | lfgredgge2 28381* | An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ & β’ πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} β β’ ((πΌ:π΄βΆπΈ β§ π β π΄) β 2 β€ (β―β(πΌβπ))) | ||
Theorem | lfgrnloop 28382* | A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π΄ = dom πΌ & β’ πΈ = {π₯ β π« π β£ 2 β€ (β―βπ₯)} β β’ (πΌ:π΄βΆπΈ β {π₯ β π΄ β£ (πΌβπ₯) = {π}} = β ) | ||
Theorem | uhgredgiedgb 28383* | In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UHGraph β (πΈ β (EdgβπΊ) β βπ₯ β dom πΌ πΈ = (πΌβπ₯))) | ||
Theorem | uhgriedg0edg0 28384 | 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 28385 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) |
β’ ((πΊ β UHGraph β§ πΈ β (EdgβπΊ)) β πΈ β (π« (VtxβπΊ) β {β })) | ||
Theorem | edguhgr 28386 | 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 28387 | 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 28388 | 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 28389* | 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βπΊ) β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | umgredgss 28390* | 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βπΊ) β£ (β―βπ₯) = 2}) | ||
Theorem | edgupgr 28391 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) |
β’ ((πΊ β UPGraph β§ πΈ β (EdgβπΊ)) β (πΈ β π« (VtxβπΊ) β§ πΈ β β β§ (β―βπΈ) β€ 2)) | ||
Theorem | edgumgr 28392 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) |
β’ ((πΊ β UMGraph β§ πΈ β (EdgβπΊ)) β (πΈ β π« (VtxβπΊ) β§ (β―βπΈ) = 2)) | ||
Theorem | uhgrvtxedgiedgb 28393* | 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.) (Revised by AV, 6-Jul-2022.) |
β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π β π) β (βπ β dom πΌ π β (πΌβπ) β βπ β πΈ π β π)) | ||
Theorem | upgredg 28394* | 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 28395* | 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 28396 | 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 28397 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 28364. 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 4769 or prprc2 4770, i.e. a loop), but π β π or π β π would not be true. (Contributed by AV, 27-Nov-2020.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ {π, π} β πΈ) β (π β π β§ π β π)) | ||
Theorem | upgredg2vtx 28398* | 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 28399 | 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 28400* | 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 β§ π β π) β (βͺ π£ β (π β {π}){π β dom πΈ β£ (π β (πΈβπ) β§ π£ β (πΈβπ))} βͺ {π β dom πΈ β£ (πΈβπ) = {π}}) = {π β dom πΈ β£ π β (πΈβπ)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |