HomeTheorem List (p. 286 of 479)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 286 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: | Metamath Proof Explorer
(1-30171) |
Hilbert Space Explorer
(30172-31694) |
Users' Mathboxes
(31695-47852) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | uspgr1e 28501 | 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 28502 | 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 28503 | 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 28504 | 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 28505 | 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 28506 | A simple pseudograph with (at least) one vertex and one edge (a loop). (Contributed by AV, 5-Dec-2020.) |
| β’ ((π β π β§ π΄ β π β§ π΅ β π) β β¨π, {β¨π΄, {π΅}β©}β© β USPGraph) | ||
| Theorem | usgr1eop 28507 | 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 28508 | A simple pseudograph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
| β’ ((π΄ β π β§ π΅ β π) β β¨{π΄, π΅}, β¨β{π΄, π΅}ββ©β© β USPGraph) | ||
| Theorem | usgr2v1e2w 28509 | A simple graph with two vertices and one edge represented by a singleton word. (Contributed by AV, 9-Jan-2021.) |
| β’ ((π΄ β π β§ π΅ β π β§ π΄ β π΅) β β¨{π΄, π΅}, β¨β{π΄, π΅}ββ©β© β USGraph) | ||
| Theorem | edg0usgr 28510 | 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 28511* | 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 28512 | 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 28513 | 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 28514 | 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 28515 | Lemma for usgrexmpledg 28519: 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 28516* | Lemma for usgrexmpl 28520. (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 28517 | Lemma for usgrexmpl 28520. (Contributed by AV, 21-Oct-2020.) |
| β’ π = (0...4) & β’ πΈ = β¨β{0, 1} {1, 2} {2, 0} {0, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((VtxβπΊ) = π β§ (iEdgβπΊ) = πΈ) | ||
| Theorem | usgrexmplvtx 28518 | 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 28519 | 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 28520 | πΊ 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 28521* | The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020.) |
| β’ π = {β¨π£, πβ© β£ π:β βΆβ } β β’ π β V | ||
| Theorem | griedg0ssusgr 28522* | 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 28523 | The class of simple graphs is a proper class (and therefore, because of prcssprc 5326, the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020.) |
| β’ USGraph β V | ||
| Syntax | csubgr 28524 | Extend class notation with subgraphs. |
| class SubGraph | ||
| Definition | df-subgr 28525* | Define the class of the subgraph relation. A class π is a subgraph of a class π (the supergraph of π ) if its vertices are also vertices of π, and its edges are also edges of π, connecting vertices of π only (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). The second condition is ensured by the requirement that the edge function of π is a restriction of the edge function of π having only vertices of π in its range. Note that the domains of the edge functions of the subgraph and the supergraph should be compatible. (Contributed by AV, 16-Nov-2020.) |
| β’ SubGraph = {β¨π , πβ© β£ ((Vtxβπ ) β (Vtxβπ) β§ (iEdgβπ ) = ((iEdgβπ) βΎ dom (iEdgβπ )) β§ (Edgβπ ) β π« (Vtxβπ ))} | ||
| Theorem | relsubgr 28526 | The class of the subgraph relation is a relation. (Contributed by AV, 16-Nov-2020.) |
| β’ Rel SubGraph | ||
| Theorem | subgrv 28527 | If a class is a subgraph of another class, both classes are sets. (Contributed by AV, 16-Nov-2020.) |
| β’ (π SubGraph πΊ β (π β V β§ πΊ β V)) | ||
| Theorem | issubgr 28528 | The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΌ = (iEdgβπ) & β’ π΅ = (iEdgβπΊ) & β’ πΈ = (Edgβπ) β β’ ((πΊ β π β§ π β π) β (π SubGraph πΊ β (π β π΄ β§ πΌ = (π΅ βΎ dom πΌ) β§ πΈ β π« π))) | ||
| Theorem | issubgr2 28529 | The property of a set to be a subgraph of a set whose edge function is actually a function. (Contributed by AV, 20-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΌ = (iEdgβπ) & β’ π΅ = (iEdgβπΊ) & β’ πΈ = (Edgβπ) β β’ ((πΊ β π β§ Fun π΅ β§ π β π) β (π SubGraph πΊ β (π β π΄ β§ πΌ β π΅ β§ πΈ β π« π))) | ||
| Theorem | subgrprop 28530 | The properties of a subgraph. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΌ = (iEdgβπ) & β’ π΅ = (iEdgβπΊ) & β’ πΈ = (Edgβπ) β β’ (π SubGraph πΊ β (π β π΄ β§ πΌ = (π΅ βΎ dom πΌ) β§ πΈ β π« π)) | ||
| Theorem | subgrprop2 28531 | The properties of a subgraph: If π is a subgraph of πΊ, its vertices are also vertices of πΊ, and its edges are also edges of πΊ, connecting vertices of the subgraph only. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΌ = (iEdgβπ) & β’ π΅ = (iEdgβπΊ) & β’ πΈ = (Edgβπ) β β’ (π SubGraph πΊ β (π β π΄ β§ πΌ β π΅ β§ πΈ β π« π)) | ||
| Theorem | uhgrissubgr 28532 | The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΌ = (iEdgβπ) & β’ π΅ = (iEdgβπΊ) β β’ ((πΊ β π β§ Fun π΅ β§ π β UHGraph) β (π SubGraph πΊ β (π β π΄ β§ πΌ β π΅))) | ||
| Theorem | subgrprop3 28533 | The properties of a subgraph: If π is a subgraph of πΊ, its vertices are also vertices of πΊ, and its edges are also edges of πΊ. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ π΄ = (VtxβπΊ) & β’ πΈ = (Edgβπ) & β’ π΅ = (EdgβπΊ) β β’ (π SubGraph πΊ β (π β π΄ β§ πΈ β π΅)) | ||
| Theorem | egrsubgr 28534 | An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 17-Dec-2020.) |
| β’ (((πΊ β π β§ π β π) β§ (Vtxβπ) β (VtxβπΊ) β§ (Fun (iEdgβπ) β§ (Edgβπ) = β )) β π SubGraph πΊ) | ||
| Theorem | 0grsubgr 28535 | The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) |
| β’ (πΊ β π β β SubGraph πΊ) | ||
| Theorem | 0uhgrsubgr 28536 | The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 28-Nov-2020.) |
| β’ ((πΊ β π β§ π β UHGraph β§ (Vtxβπ) = β ) β π SubGraph πΊ) | ||
| Theorem | uhgrsubgrself 28537 | A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
| β’ (πΊ β UHGraph β πΊ SubGraph πΊ) | ||
| Theorem | subgrfun 28538 | The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020.) |
| β’ ((Fun (iEdgβπΊ) β§ π SubGraph πΊ) β Fun (iEdgβπ)) | ||
| Theorem | subgruhgrfun 28539 | The edge function of a subgraph of a hypergraph is a function. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 20-Nov-2020.) |
| β’ ((πΊ β UHGraph β§ π SubGraph πΊ) β Fun (iEdgβπ)) | ||
| Theorem | subgreldmiedg 28540 | An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020.) |
| β’ ((π SubGraph πΊ β§ π β dom (iEdgβπ)) β π β dom (iEdgβπΊ)) | ||
| Theorem | subgruhgredgd 28541 | An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ πΌ = (iEdgβπ) & β’ (π β πΊ β UHGraph) & β’ (π β π SubGraph πΊ) & β’ (π β π β dom πΌ) β β’ (π β (πΌβπ) β (π« π β {β })) | ||
| Theorem | subumgredg2 28542* | An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.) |
| β’ π = (Vtxβπ) & β’ πΌ = (iEdgβπ) β β’ ((π SubGraph πΊ β§ πΊ β UMGraph β§ π β dom πΌ) β (πΌβπ) β {π β π« π β£ (β―βπ) = 2}) | ||
| Theorem | subuhgr 28543 | A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
| β’ ((πΊ β UHGraph β§ π SubGraph πΊ) β π β UHGraph) | ||
| Theorem | subupgr 28544 | A subgraph of a pseudograph is a pseudograph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
| β’ ((πΊ β UPGraph β§ π SubGraph πΊ) β π β UPGraph) | ||
| Theorem | subumgr 28545 | A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.) |
| β’ ((πΊ β UMGraph β§ π SubGraph πΊ) β π β UMGraph) | ||
| Theorem | subusgr 28546 | A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 27-Nov-2020.) |
| β’ ((πΊ β USGraph β§ π SubGraph πΊ) β π β USGraph) | ||
| Theorem | uhgrspansubgrlem 28547 | Lemma for uhgrspansubgr 28548: The edges of the graph π obtained by removing some edges of a hypergraph πΊ are subsets of its vertices (a spanning subgraph, see comment for uhgrspansubgr 28548. (Contributed by AV, 18-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β UHGraph) β β’ (π β (Edgβπ) β π« (Vtxβπ)) | ||
| Theorem | uhgrspansubgr 28548 | A spanning subgraph π of a hypergraph πΊ is actually a subgraph of πΊ. A subgraph π of a graph πΊ which has the same vertices as πΊ and is obtained by removing some edges of πΊ is called a spanning subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β UHGraph) β β’ (π β π SubGraph πΊ) | ||
| Theorem | uhgrspan 28549 | A spanning subgraph π of a hypergraph πΊ is a hypergraph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β UHGraph) β β’ (π β π β UHGraph) | ||
| Theorem | upgrspan 28550 | A spanning subgraph π of a pseudograph πΊ is a pseudograph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β UPGraph) β β’ (π β π β UPGraph) | ||
| Theorem | umgrspan 28551 | A spanning subgraph π of a multigraph πΊ is a multigraph. (Contributed by AV, 27-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β UMGraph) β β’ (π β π β UMGraph) | ||
| Theorem | usgrspan 28552 | A spanning subgraph π of a simple graph πΊ is a simple graph. (Contributed by AV, 15-Oct-2020.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ (π β π β π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΈ βΎ π΄)) & β’ (π β πΊ β USGraph) β β’ (π β π β USGraph) | ||
| Theorem | uhgrspanop 28553 | A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UHGraph β β¨π, (πΈ βΎ π΄)β© β UHGraph) | ||
| Theorem | upgrspanop 28554 | A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UPGraph β β¨π, (πΈ βΎ π΄)β© β UPGraph) | ||
| Theorem | umgrspanop 28555 | A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β UMGraph β β¨π, (πΈ βΎ π΄)β© β UMGraph) | ||
| Theorem | usgrspanop 28556 | A spanning subgraph of a simple graph represented by an ordered pair is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) β β’ (πΊ β USGraph β β¨π, (πΈ βΎ π΄)β© β USGraph) | ||
| Theorem | uhgrspan1lem1 28557 | Lemma 1 for uhgrspan1 28560. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = {π β dom πΌ β£ π β (πΌβπ)} β β’ ((π β {π}) β V β§ (πΌ βΎ πΉ) β V) | ||
| Theorem | uhgrspan1lem2 28558 | Lemma 2 for uhgrspan1 28560. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = {π β dom πΌ β£ π β (πΌβπ)} & β’ π = β¨(π β {π}), (πΌ βΎ πΉ)β© β β’ (Vtxβπ) = (π β {π}) | ||
| Theorem | uhgrspan1lem3 28559 | Lemma 3 for uhgrspan1 28560. (Contributed by AV, 19-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = {π β dom πΌ β£ π β (πΌβπ)} & β’ π = β¨(π β {π}), (πΌ βΎ πΉ)β© β β’ (iEdgβπ) = (πΌ βΎ πΉ) | ||
| Theorem | uhgrspan1 28560* | The induced subgraph π of a hypergraph πΊ obtained by removing one vertex is actually a subgraph of πΊ. A subgraph is called induced or spanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). (Contributed by AV, 19-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = {π β dom πΌ β£ π β (πΌβπ)} & β’ π = β¨(π β {π}), (πΌ βΎ πΉ)β© β β’ ((πΊ β UHGraph β§ π β π) β π SubGraph πΊ) | ||
| Theorem | upgrreslem 28561* | Lemma for upgrres 28563. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = {π β dom πΈ β£ π β (πΈβπ)} β β’ ((πΊ β UPGraph β§ π β π) β ran (πΈ βΎ πΉ) β {π β (π« (π β {π}) β {β }) β£ (β―βπ) β€ 2}) | ||
| Theorem | umgrreslem 28562* | Lemma for umgrres 28564 and usgrres 28565. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = {π β dom πΈ β£ π β (πΈβπ)} β β’ ((πΊ β UMGraph β§ π β π) β ran (πΈ βΎ πΉ) β {π β π« (π β {π}) β£ (β―βπ) = 2}) | ||
| Theorem | upgrres 28563* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 28560) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = β¨(π β {π}), (πΈ βΎ πΉ)β© β β’ ((πΊ β UPGraph β§ π β π) β π β UPGraph) | ||
| Theorem | umgrres 28564* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 28560) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = β¨(π β {π}), (πΈ βΎ πΉ)β© β β’ ((πΊ β UMGraph β§ π β π) β π β UMGraph) | ||
| Theorem | usgrres 28565* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 28560) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 19-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (iEdgβπΊ) & β’ πΉ = {π β dom πΈ β£ π β (πΈβπ)} & β’ π = β¨(π β {π}), (πΈ βΎ πΉ)β© β β’ ((πΊ β USGraph β§ π β π) β π β USGraph) | ||
| Theorem | upgrres1lem1 28566* | Lemma 1 for upgrres1 28570. (Contributed by AV, 7-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} β β’ ((π β {π}) β V β§ ( I βΎ πΉ) β V) | ||
| Theorem | umgrres1lem 28567* | Lemma for umgrres1 28571. (Contributed by AV, 27-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} β β’ ((πΊ β UMGraph β§ π β π) β ran ( I βΎ πΉ) β {π β π« (π β {π}) β£ (β―βπ) = 2}) | ||
| Theorem | upgrres1lem2 28568* | Lemma 2 for upgrres1 28570. (Contributed by AV, 7-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ (Vtxβπ) = (π β {π}) | ||
| Theorem | upgrres1lem3 28569* | Lemma 3 for upgrres1 28570. (Contributed by AV, 7-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ (iEdgβπ) = ( I βΎ πΉ) | ||
| Theorem | upgrres1 28570* | A pseudograph obtained by removing one vertex and all edges incident with this vertex is a pseudograph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 28525 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ ((πΊ β UPGraph β§ π β π) β π β UPGraph) | ||
| Theorem | umgrres1 28571* | A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 28525 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ ((πΊ β UMGraph β§ π β π) β π β UMGraph) | ||
| Theorem | usgrres1 28572* | Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted graph is not a subgraph of the original graph in the sense of df-subgr 28525 since the domains of the edge functions may not be compatible. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} & β’ π = β¨(π β {π}), ( I βΎ πΉ)β© β β’ ((πΊ β USGraph β§ π β π) β π β USGraph) | ||
| Syntax | cfusgr 28573 | Extend class notation with finite simple graphs. |
| class FinUSGraph | ||
| Definition | df-fusgr 28574 | Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite simple graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
| β’ FinUSGraph = {π β USGraph β£ (Vtxβπ) β Fin} | ||
| Theorem | isfusgr 28575 | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
| β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β (πΊ β USGraph β§ π β Fin)) | ||
| Theorem | fusgrvtxfi 28576 | A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.) |
| β’ π = (VtxβπΊ) β β’ (πΊ β FinUSGraph β π β Fin) | ||
| Theorem | isfusgrf1 28577* | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (πΊ β FinUSGraph β (πΌ:dom πΌβ1-1β{π₯ β π« π β£ (β―βπ₯) = 2} β§ π β Fin))) | ||
| Theorem | isfusgrcl 28578 | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 9-Jan-2020.) |
| β’ (πΊ β FinUSGraph β (πΊ β USGraph β§ (β―β(VtxβπΊ)) β β0)) | ||
| Theorem | fusgrusgr 28579 | A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
| β’ (πΊ β FinUSGraph β πΊ β USGraph) | ||
| Theorem | opfusgr 28580 | A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.) |
| β’ ((π β π β§ πΈ β π) β (β¨π, πΈβ© β FinUSGraph β (β¨π, πΈβ© β USGraph β§ π β Fin))) | ||
| Theorem | usgredgffibi 28581 | The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 22-Oct-2020.) |
| β’ πΌ = (iEdgβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β USGraph β (πΈ β Fin β πΌ β Fin)) | ||
| Theorem | fusgredgfi 28582* | In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 21-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FinUSGraph β§ π β π) β {π β πΈ β£ π β π} β Fin) | ||
| Theorem | usgr1v0e 28583 | The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 22-Oct-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ (β―βπ) = 1) β (β―βπΈ) = 0) | ||
| Theorem | usgrfilem 28584* | In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΉ = {π β πΈ β£ π β π} β β’ ((πΊ β FinUSGraph β§ π β π) β (πΈ β Fin β πΉ β Fin)) | ||
| Theorem | fusgrfisbase 28585 | Induction base for fusgrfis 28587. Main work is done in uhgr0v0e 28495. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
| β’ (((π β π β§ πΈ β π) β§ β¨π, πΈβ© β USGraph β§ (β―βπ) = 0) β πΈ β Fin) | ||
| Theorem | fusgrfisstep 28586* | Induction step in fusgrfis 28587: In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
| β’ (((π β π β§ πΈ β π) β§ β¨π, πΈβ© β FinUSGraph β§ π β π) β (( I βΎ {π β (Edgββ¨π, πΈβ©) β£ π β π}) β Fin β πΈ β Fin)) | ||
| Theorem | fusgrfis 28587 | A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 8-Nov-2020.) |
| β’ (πΊ β FinUSGraph β (EdgβπΊ) β Fin) | ||
| Theorem | fusgrfupgrfs 28588 | A finite simple graph is a finite pseudograph of finite size. (Contributed by AV, 27-Dec-2021.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β FinUSGraph β (πΊ β UPGraph β§ π β Fin β§ πΌ β Fin)) | ||
| Syntax | cnbgr 28589 | Extend class notation with neighbors (of a vertex in a graph). |
| class NeighbVtx | ||
| Definition | df-nbgr 28590* |
Define the (open) neighborhood resp. the class of all neighbors of a
vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or
definition in section 1.1 of [Diestel]
p. 3. The neighborhood/neighbors
of a vertex are all (other) vertices which are connected with this
vertex by an edge. In contrast to a closed neighborhood, a vertex is
not a neighbor of itself. This definition is applicable even for
arbitrary hypergraphs.
Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei 22602), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.) |
| β’ NeighbVtx = (π β V, π£ β (Vtxβπ) β¦ {π β ((Vtxβπ) β {π£}) β£ βπ β (Edgβπ){π£, π} β π}) | ||
| Theorem | nbgrprc0 28591 | The set of neighbors is empty if the graph πΊ or the vertex π are proper classes. (Contributed by AV, 26-Oct-2020.) |
| β’ (Β¬ (πΊ β V β§ π β V) β (πΊ NeighbVtx π) = β ) | ||
| Theorem | nbgrcl 28592 | If a class π has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021.) (Revised by AV, 12-Feb-2022.) |
| β’ π = (VtxβπΊ) β β’ (π β (πΊ NeighbVtx π) β π β π) | ||
| Theorem | nbgrval 28593* | The set of neighbors of a vertex π in a graph πΊ. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by AV, 21-Mar-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β π β (πΊ NeighbVtx π) = {π β (π β {π}) β£ βπ β πΈ {π, π} β π}) | ||
| Theorem | dfnbgr2 28594* | Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020.) (Revised by AV, 21-Mar-2021.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β π β (πΊ NeighbVtx π) = {π β (π β {π}) β£ βπ β πΈ (π β π β§ π β π)}) | ||
| Theorem | dfnbgr3 28595* | Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 28593). (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 25-Oct-2020.) (Revised by AV, 21-Mar-2021.) |
| β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((π β π β§ Fun πΌ) β (πΊ NeighbVtx π) = {π β (π β {π}) β£ βπ β dom πΌ{π, π} β (πΌβπ)}) | ||
| Theorem | nbgrnvtx0 28596 | If a class π is not a vertex of a graph πΊ, then it has no neighbors in πΊ. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
| β’ π = (VtxβπΊ) β β’ (π β π β (πΊ NeighbVtx π) = β ) | ||
| Theorem | nbgrel 28597* | Characterization of a neighbor π of a vertex π in a graph πΊ. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (πΊ NeighbVtx π) β ((π β π β§ π β π) β§ π β π β§ βπ β πΈ {π, π} β π)) | ||
| Theorem | nbgrisvtx 28598 | Every neighbor π of a vertex πΎ is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.) |
| β’ π = (VtxβπΊ) β β’ (π β (πΊ NeighbVtx πΎ) β π β π) | ||
| Theorem | nbgrssvtx 28599 | The neighbors of a vertex πΎ in a graph form a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.) |
| β’ π = (VtxβπΊ) β β’ (πΊ NeighbVtx πΎ) β π | ||
| Theorem | nbuhgr 28600* | The set of neighbors of a vertex in a hypergraph. This version of nbgrval 28593 (with π being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.) |
| β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ π β π) β (πΊ NeighbVtx π) = {π β (π β {π}) β£ βπ β πΈ {π, π} β π}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |