Home | Metamath
Proof ExplorerTheorem List
(p. 282 of 322)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21498) |
Hilbert Space Explorer
(21499-23021) |
Users' Mathboxes
(23022-32154) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | usgrav 28101 | The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |

USGrph | ||

Theorem | isuslgra 28102* | The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USLGrph | ||

Theorem | isusgra 28103* | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph | ||

Theorem | uslgraf 28104* | The edge function of an undirected simple graph with loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USLGrph | ||

Theorem | usgraf 28105* | The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph | ||

Theorem | isusgra0 28106* | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

USGrph | ||

Theorem | usgraf0 28107* | The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

USGrph | ||

Theorem | usgrafun 28108 | The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) |

USGrph | ||

Theorem | usgraedgop 28109 | An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) |

USGrph | ||

Theorem | usgrass 28110 | An edge is a subset of vertices, analogous to umgrass 23871. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |

USGrph | ||

Theorem | usgraeq12d 28111 | Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.) |

USGrph USGrph | ||

Theorem | uslisumgra 28112 | An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USLGrph UMGrph | ||

Theorem | usisuslgra 28113 | An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph USLGrph | ||

Theorem | usisumgra 28114 | An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) |

USGrph UMGrph | ||

Theorem | usgrares 28115 | A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 23876. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph USGrph | ||

Theorem | usgra0 28116 | The empty graph, with vertices but no edges, is a graph, analogous to umgra0 23877. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph | ||

Theorem | usgra0v 28117 | The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |

USGrph | ||

Theorem | uslgra1 28118 | The graph with one edge, analogous to umgra1 23878. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USLGrph | ||

Theorem | usgra1 28119 | The graph with one edge, analogous to umgra1 23878 ( with additional assumption that since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USGrph | ||

Theorem | uslgraun 28120 | If and are (simple) graphs (with loops), then is a multigraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices), analogous to umgraun 23879. (Contributed by Alexander van der Vekens, 10-Aug-2017.) |

USLGrph USLGrph UMGrph | ||

Theorem | usgraedg2 28121 | The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 23873. (Contributed by Alexander van der Vekens, 11-Aug-2017.) |

USGrph | ||

Theorem | usgraedgprv 28122 | In an undirected graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |

USGrph | ||

Theorem | usgraedgrnv 28123 | An edge of an undirected simple graph always connects to vertices. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |

USGrph | ||

Theorem | usgranloop 28124* | In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) |

USGrph | ||

Theorem | usgraedgrn 28125 | An edge of an undirected simple graph without loops always connects two different vertices. (Contributed by Alexander van der Vekens, 2-Sep-2017.) |

USGrph | ||

18.23.3.8 Undirected simple graphs
(examples) | ||

Theorem | usgra1v 28126 | A class with one (or no) vertex is a graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |

USGrph | ||

Theorem | usgraexvlem 28127 | Lemma for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

Theorem | usgraex0elv 28128 | Lemma 0 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

Theorem | usgraex1elv 28129 | Lemma 1 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

Theorem | usgraex2elv 28130 | Lemma 2 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

Theorem | usgraex3elv 28131 | Lemma 3 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |

Theorem | usgraexmpldifpr 28132 | Lemma for usgraexmpl 28133: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |

Theorem | usgraexmpl 28133 | is a graph of five vertices , with edges . (Contributed by Alexander van der Vekens, 15-Aug-2017.) |

USGrph | ||

18.23.3.9 Neighbors, complete graphs and
universal vertices | ||

Syntax | cnbgra 28134 | Extend class notation with Neighbors (of a vertex in a graph). |

Neighbors | ||

Syntax | ccusgra 28135 | Extend class notation with complete (undirected simple) graphs. |

ComplUSGrph | ||

Syntax | cuvtx 28136 | Extend class notation with the universal vertices (in a graph). |

UnivVertex | ||

Definition | df-nbgra 28137* | Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) |

Neighbors | ||

Definition | df-cusgra 28138* | Define the class of all complete (undirected simple) graphs. A undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

ComplUSGrph USGrph | ||

Definition | df-uvtx 28139* | Define the class of all universal vertices (in a graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph). (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | nbgraop 28140* | The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |

Neighbors | ||

Theorem | nbgrael 28141 | The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) |

Neighbors | ||

Theorem | nbgranv0 28142 | There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

Neighbors | ||

Theorem | nbusgra 28143* | The set of neighbors of a vertex in a graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgra0nb 28144* | A vertex which is not endpoint of an edge has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgraeledg 28145 | A class/vertex is a neighbor of another class/vertex if and only if it is an endpoint of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgraisvtx 28146 | Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgra0edg 28147 | In a graph with no edges, every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgrassvt 28148 | The neighbors of a node in a graph are a subset of all nodes of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgranself 28149* | A node in a graph (without loops!) is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgrassovt 28150 | The neighbors of a vertex are a subset of the other vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgranself2 28151 | A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors | ||

Theorem | nbgrasym 28152 | A vertex in a graph is a neighbor of a second vertex if and only if the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph Neighbors Neighbors | ||

Theorem | iscusgra 28153* | The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

ComplUSGrph USGrph | ||

Theorem | iscusgra0 28154* | The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |

ComplUSGrph USGrph | ||

Theorem | cusisusgra 28155 | A complete (undirected simple) graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |

ComplUSGrph USGrph | ||

Theorem | cusgra0v 28156 | A graph with no vertices (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |

ComplUSGrph | ||

Theorem | cusgra1v 28157 | A graph with one vertex (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) |

ComplUSGrph | ||

Theorem | cusgra2v 28158 | A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

USGrph ComplUSGrph | ||

Theorem | nbcusgra 28159 | In a complete (undirected simple) graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

ComplUSGrph Neighbors | ||

Theorem | isuvtx 28160* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | uvtxel 28161* | An element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | uvtxisvtx 28162 | A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | uvtx0 28163 | There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | uvtx01vtx 28164* | If a graph/class has no edges, it has universal vertices if and only if it has at most one vertex. This theorem could have been stated UnivVertex , but a lot of auxiliary theorems would have been needed. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |

UnivVertex | ||

Theorem | uvtxnbgra 28165 | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |

USGrph UnivVertex Neighbors | ||

Theorem | uvtxnm1nbgra 28166 | A universal vertex has neighbors in a graph with vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |

USGrph UnivVertex Neighbors | ||

Theorem | uvtxnbgravtx 28167* | A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |

USGrph UnivVertex Neighbors | ||

Theorem | cusgrauvtx 28168 | In a complete (undirected simple) graph, each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |

ComplUSGrph UnivVertex | ||

18.23.3.10 Friendship graphsIn this section, the basics for the friendship theorem, which is one from the "100 theorem list" (#83), are provided, including the definition of friendship graphs df-frgra 28170 as special undirected simple graphs without loops (see frisusgra 28173) and the proofs of the friendship theorem for small graphs (with up to 3 vertices), see 1to3vfriendship 28186. The general friendship theorem, which should be called "friendship", but which is still to be proven, would be FriendGrph . The case (a graph without vertices) must be excluded either from the definition of a friendship graph, or from the theorem. If it is not excluded from the definition, which is the case with df-frgra 28170, a graph without vertices is a friendship graph (see frgra0 28175), but the friendship condition does not hold (because of , see rex0 3468). Further results of this sections are: Any graph with exactly one vertex is a friendship graph, see frgra1v 28176, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 28177, a graph with exactly 3 (different) vertices is a friendship graph if and only if it is a complete graph (every two vertices are connected by an edge), see frgra3v 28180, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 28185 (The generalization of this theorem "Every friendship graph (with at least one vertex) is a windmill graph" is a stronger result than the "friendship theorem" which was proven by Mertzios and Unger, see "The friendship problem on graphs", ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp 152-158). | ||

Syntax | cfrgra 28169 | Extend class notation with Friendship Graphs. |

FriendGrph | ||

Definition | df-frgra 28170* | Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | isfrgra 28171* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | frisusgrapr 28172* | A friendship graph is an undirected simple graph without loops with special properties. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | frisusgra 28173 | A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | frgra0v 28174 | Any graph with no vertex is a friendship graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph | ||

Theorem | frgra0 28175 | Any empty graph (graph without vertices) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |

FriendGrph | ||

Theorem | frgra1v 28176 | Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

USGrph FriendGrph | ||

Theorem | frgra2v 28177 | Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |

FriendGrph | ||

Theorem | frgra3vlem1 28178* | Lemma 1 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

USGrph | ||

Theorem | frgra3vlem2 28179* | Lemma 2 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

USGrph | ||

Theorem | frgra3v 28180 | Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |

USGrph FriendGrph | ||

Theorem | 1vwmgra 28181* | Every graph with one vertex is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |

Theorem | 3vfriswmgralem 28182* | Lemma for 3vfriswmgra 28183. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |

USGrph | ||

Theorem | 3vfriswmgra 28183* | Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |

FriendGrph | ||

Theorem | 1to2vfriswmgra 28184* | Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |

FriendGrph | ||

Theorem | 1to3vfriswmgra 28185* | Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |

FriendGrph | ||

Theorem | 1to3vfriendship 28186* | The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |

FriendGrph | ||

18.24 Mathbox for David A.
Wheeler
This is the mathbox of David A. Wheeler, dwheeler at dwheeler dot com.
Among other things, I have added a number of formal definitions for
widely-used functions, e.g., those defined in
ISO 80000-2:2009(E)
| ||

18.24.1 Natural deduction | ||

Theorem | 19.8ad 28187 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1718. (Contributed by DAW, 13-Feb-2017.) |

Theorem | sbidd 28188 | An identity theorem for substitution. See sbid 1863. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) |

Theorem | sbidd-misc 28189 | An identity theorem for substitution. See sbid 1863. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) |

18.24.2 Greater than, greater than or equal
to.As a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to reduce the number of conversion steps. Here we formally define the widely-used relations 'greater than' and 'greater than or equal to', so that we have formal definitions of them, as well as a few related theorems. | ||

Syntax | cge-real 28190 | Extend wff notation to include the 'greater than or equal to' relation, see df-gte 28192. |

Syntax | cgt 28191 | Extend wff notation to include the 'greater than' relation, see df-gt 28193. |

Definition | df-gte 28192 |
Define the 'greater than or equal' predicate over the reals. Defined in
ISO 80000-2:2009(E) operation 2-7.10. It is used as a primitive in the
"NIST Digital Library of Mathematical Functions" , front
introduction,
"Common Notations and Definitions" section at
http://dlmf.nist.gov/front/introduction#Sx4.
This relation is merely
the converse of the 'less than or equal to' relation defined by df-le 8873.
We do not write this as , and similarly we do
not write ` > ` as , because these are not
definitional axioms as understood by mmj2 (those definitions will be
flagged as being "potentially non-conservative"). We could
write them
this way:
and
but
these are very complicated. This definition of , and the similar
one for (df-gt 28193), are a bit strange when you see them for
the
first time, but these definitions are much simpler for us to process and
are clearly conservative definitions. (My thanks to Mario Carneiro for
pointing out this simpler approach.) See gte-lte 28194 for a more
conventional expression of the relationship between and . As
a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to
reduce the number of conversion steps. Thus, we discourage its use, but
include its definition so that there (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Definition | df-gt 28193 |
The 'greater than' relation is merely the converse of the 'less than or
equal to' relation defined by df-lt 8750. Defined in ISO 80000-2:2009(E)
operation 2-7.12. See df-gte 28192 for a discussion on why this approach is
used for the definition. See gt-lt 28195 and gt-lth 28197 for more conventional
expression of the relationship between and .
As a stylistic issue, set.mm prefers 'less than or equal' instead of
'greater than or equal' to reduce the number of conversion steps. Thus,
we discourage its use, but include its definition so that there (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | gte-lte 28194 | Simple relationship between and . (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Theorem | gt-lt 28195 | Simple relationship between and . (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | gte-lteh 28196 | Relationship between and using hypotheses. (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

Theorem | gt-lth 28197 | Relationship between and using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015.) (New usage is discouraged.) |

Theorem | ex-gt 28198 | Simple example of , in this case, 0 is not greater than 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.) |

Theorem | ex-gte 28199 | Simple example of , in this case, 0 is greater than or equal to 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017.) (New usage is discouraged.) |

18.24.3 Hyperbolic trig functionsIt is a convention of set.mm to not use sinh and so on directly, and instead of use expansions such as . However, I believe it's important to give formal definitions for these conventional functions as they are typically used, so here they are. A few related identities are also proved. | ||

Syntax | csinh 28200 | Extend class notation to include the hyperbolic sine function, see df-sinh 28203. |

sinh |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |