Home | Metamath
Proof ExplorerTheorem List
(p. 284 of 327)
| < 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-22413) |
Hilbert Space Explorer
(22414-23936) |
Users' Mathboxes
(23937-32699) |

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

Statement | ||

Theorem | el2pthsot 28301* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |

2SPathOnOt SPaths | ||

Theorem | el2wlksotot 28302* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 26-Feb-2018.) |

2WalksOt Walks | ||

Theorem | usg2wlkonot 28303 | A walk of length 2 between two vertices as ordered triple in an undirected simple graph. This theorem would also hold for undirected multigraphs, but to proof this the cases and/or must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

USGrph 2WalksOnOt | ||

Theorem | usg2wotspth 28304* | A walk of length 2 between two different vertices as ordered triple corresponds to a simple path of length 2 in an undirected simple graph. (Contributed by Alexander van der Vekens, 16-Feb-2018.) |

USGrph 2WalksOnOt SPaths | ||

Theorem | 2pthwlkonot 28305 | For two different vertices, a walk of length 2 between these vertices as ordered triple is a simple path of length 2 between these vertices as ordered triple in an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |

USGrph 2SPathOnOt 2WalksOnOt | ||

Theorem | 2wot2wont 28306* | The set of (simple) paths of length 2 (in a graph) is the set of (simple) paths of length 2 between any two different vertices. (Contributed by Alexander van der Vekens, 27-Feb-2018.) |

2WalksOt 2WalksOnOt | ||

Theorem | 2spontn0vne 28307 | If the set of simple paths of length 2 between two vertices (in a graph) is not empty, the two vertices must be not equal. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |

2SPathOnOt | ||

Theorem | usg2spthonot 28308 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |

USGrph 2SPathOnOt | ||

Theorem | usg2spthonot0 28309 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |

USGrph 2SPathOnOt | ||

Theorem | usg2spthonot1 28310* | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |

USGrph 2SPathOnOt | ||

Theorem | 2spot2iun2spont 28311* | The set of simple paths of length 2 (in a graph) is the double union of the simple paths of length 2 between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |

2SPathOnOt 2SPathOnOt | ||

Theorem | 2spotfi 28312 | In a finite graph, the set of simple paths of length 2 between two vertices (as ordered triples) is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |

2SPathOnOt | ||

19.22.4.6 Vertex Degree | ||

Theorem | usgfidegfi 28313* | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

USGrph VDeg | ||

Theorem | usgfiregdegfi 28314* | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |

USGrph VDeg | ||

19.22.4.7 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 28316 as special undirected simple graphs without loops (see frisusgra 28319) and the proofs of the friendship theorem for small graphs (with up to 3 vertices), see 1to3vfriendship 28335. 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 28316, a graph without vertices is a friendship graph (see frgra0 28321), but the friendship condition does not hold (because of , see rex0 3633). Further results of this sections are: Any graph with exactly one vertex is a friendship graph, see frgra1v 28325, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 28326, 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 28329, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 28334 (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". This generalization was proven by Mertzios and Unger, see Theorem 1 of [MertziosUnger] p. 152.). The first steps to prove the friendship theorem following the approach of Mertzios and Unger are already made, see 2pthfrgrarn2 28337 and n4cyclfrgra 28345 (these theorems correspond to Proposition 1 of [MertziosUnger] p. 153.). In addition, the first three Lemmas ("claims") in the proof of [Huneke] p. 1 are proven, see frgrancvvdgeq 28369, frgraregorufr 28379 and frgregordn0 28396. | ||

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

FriendGrph | ||

Definition | df-frgra 28316* | 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 28317* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | frisusgrapr 28318* | 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 28319 | A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

FriendGrph USGrph | ||

Theorem | frgra0v 28320 | 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 28321 | Any empty graph (graph without vertices) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |

FriendGrph | ||

Theorem | frgraunss 28322* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph | ||

Theorem | frgraun 28323* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph | ||

Theorem | frisusgranb 28324* | In a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph Neighbors Neighbors | ||

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

USGrph FriendGrph | ||

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

FriendGrph | ||

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

USGrph | ||

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

USGrph | ||

Theorem | frgra3v 28329 | 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 28330* | Every graph with one vertex is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |

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

USGrph | ||

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

FriendGrph | ||

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

FriendGrph | ||

Theorem | 1to3vfriswmgra 28334* | 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 28335* | 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 | ||

Theorem | 2pthfrgrarn 28336* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.) |

FriendGrph | ||

Theorem | 2pthfrgrarn2 28337* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.) |

FriendGrph | ||

Theorem | 2pthfrgra 28338* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph PathOn | ||

Theorem | 3cyclfrgrarn1 28339* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgrarn 28340* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgrarn2 28341* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017.) |

FriendGrph | ||

Theorem | 3cyclfrgra 28342* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

FriendGrph Cycles | ||

Theorem | 4cycl2v2nb 28343 | In a (maybe degenerated) 4-cycle, two vertices have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | 4cycl2vnunb 28344* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | n4cyclfrgra 28345 | There is no 4-cycle in a friendship graph, see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

FriendGrph Cycles | ||

Theorem | 4cyclusnfrgra 28346 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

USGrph FriendGrph | ||

Theorem | frgranbnb 28347 | If two neighbors of a specific vertex have a common neighbor in a friendship graph, then this common neighbor must be the specific vertex. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

Neighbors FriendGrph | ||

Theorem | frconngra 28348 | A friendship graph is connected, see 1. remark after Proposition 1 of [MertziosUnger] p. 153 : "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph ConnGrph | ||

Theorem | vdfrgra0 28349 | A vertex in a friendship graph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgfrgra0 28350 | A vertex in a friendship graph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdn0frgrav2 28351 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgn0frgrav2 28352 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdn1frgrav2 28353 | Any vertex in a friendship graph does not have degree 1, see 2. remark after Proposition 1 of [MertziosUnger] p. 153 : "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgn1frgrav2 28354 | Any vertex in a friendship graph does not have degree 1, see 2. remark after Proposition 1 of [MertziosUnger] p. 153 : "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgfrgragt2 28355 | Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see 3. remark after Proposition 1 of [MertziosUnger] p. 153 : "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | frgrancvvdeqlem1 28356* | Lemma 1 for frgrancvvdeq 28368. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem2 28357* | Lemma 2 for frgrancvvdeq 28368. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem3 28358* | Lemma 3 for frgrancvvdeq 28368. In a friendship graph, for each neighbor of a vertex there is exacly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem4 28359* | Lemma 4 for frgrancvvdeq 28368. The restricted iota of a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) |

Neighbors Neighbors FriendGrph Neighbors | ||

Theorem | frgrancvvdeqlem5 28360* | Lemma 5 for frgrancvvdeq 28368. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem6 28361* | Lemma 6 for frgrancvvdeq 28368. The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph Neighbors | ||

Theorem | frgrancvvdeqlem7 28362* | Lemma 7 for frgrancvvdeq 28368. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemA 28363* | Lemma A for frgrancvvdeq 28368. This corresponds to the following observation in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemB 28364* | Lemma B for frgrancvvdeq 28368. This corresponds to the following observation in [Huneke] p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemC 28365* | Lemma C for frgrancvvdeq 28368. This corresponds to the following observation in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem8 28366* | Lemma 8 for frgrancvvdeq 28368. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem9 28367* | Lemma 9 for frgrancvvdeq 28368. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

FriendGrph Neighbors Neighbors Neighbors | ||

Theorem | frgrancvvdeq 28368* | In a finite friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to the first Lemma ("claim") of the proof of the (friendship) theorem in [Huneke] p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph Neighbors VDeg VDeg | ||

Theorem | frgrancvvdgeq 28369* | In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to the first Lemma ("claim") of the proof of the (friendship) theorem in [Huneke] p. 1: "If x,y, are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

FriendGrph Neighbors VDeg VDeg | ||

Theorem | frgrawopreglem1 28370* | Lemma 1 for frgrawopreg 28375. In a friendship graph, the classes A and B are sets. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem2 28371* | Lemma 2 for frgrawopreg 28375. In a friendship graph with at least 2 vertices, the degree of a vertex must be at least 2. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem3 28372* | Lemma 3 for frgrawopreg 28375. The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg VDeg VDeg | ||

Theorem | frgrawopreglem4 28373* | Lemma 4 for frgrawopreg 28375. In a friendship graph each vertex with degree K is connected with a vertex with degree other than K. This corresponds to the observation in the proof of [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B." (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem5 28374* | Lemma 5 for frgrawopreg 28375. If A as well as B contain at least two vertices in a friendship graph, there is a 4-cycle in the graph. This corresponds to the observation in the proof of [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg 28375* | In a friendship graph there are either no vertices or exactly one vertex having degree K, or all or all except one vertices have degree K. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg1 28376* | According to the proof of the friendship theorem in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

VDeg FriendGrph | ||

Theorem | frgrawopreg2 28377* | According to the proof of the friendship theorem in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

VDeg FriendGrph | ||

Theorem | frgraregorufr0 28378* | For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

FriendGrph VDeg VDeg | ||

Theorem | frgraregorufr 28379* | For each nonnegative integer K there are either no edges having degree K, or all vertices have degree K in a friendship graph, unless there is a universal friend. This corresponds to the second claim in the proof of the friendship theorem in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |

FriendGrph VDeg VDeg | ||

Theorem | frgraeu 28380* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph | ||

Theorem | frg2woteu 28381* | For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2wotn0 28382 | In a friendship graph, there is always a path/walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2wot1 28383 | In a friendship graph, there is exactly one walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |

FriendGrph 2WalksOnOt | ||

Theorem | frg2spot1 28384 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |

FriendGrph 2SPathOnOt | ||

Theorem | frg2woteqm 28385 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 20-Feb-2018.) |

FriendGrph 2WalksOnOt 2WalksOnOt | ||

Theorem | frg2woteq 28386 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.) |

FriendGrph 2WalksOnOt 2WalksOnOt | ||

Theorem | 2spotdisj 28387* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |

Disj 2SPathOnOt | ||

Theorem | 2spotiundisj 28388* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) |

Disj
2SPathOnOt | ||

Theorem | frghash2spot 28389 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with vertices. This corresponds to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, the order of vertices is not respected by Huneke, so he only counts half of the paths which are existing when respecting the order as it is the case for simple paths represented by orderes triples. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |

FriendGrph 2SPathOnOt | ||

Theorem | 2spot0 28390 | If there are no vertices, then there are no paths (of length 2), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

2SPathOnOt | ||

Theorem | usg2spot2nb 28391* | The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |

2SPathOnOt USGrph Neighbors Neighbors | ||

Theorem | usgreghash2spotv 28392* | According to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For simple paths of length 2 represented by ordered triples, we have again k*(k-1) such paths. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

2SPathOnOt USGrph VDeg | ||

Theorem | usgreg2spot 28393* | In a finite k-regular graph the set of all paths of length two is the union of all the paths of length 2 over the vertices which are in the the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

2SPathOnOt USGrph VDeg 2SPathOnOt | ||

Theorem | 2spotmdisj 28394* | The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

2SPathOnOt Disj | ||

Theorem | usgreghash2spot 28395* | In a finite k-regular graph with N vertices there are N times " choose 2 " paths with length 2, according to the proof of the third claim in the proof of the friendship theorem in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by ordered triples, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

USGrph VDeg 2SPathOnOt | ||

Theorem | frgregordn0 28396* | If a nonempty friendship graph is k-regular, its order is k(k-1)+1. This corresponds to the third claim in the proof of the friendship theorem in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) |

FriendGrph VDeg | ||

19.23 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)
| ||

19.23.1 Natural deduction | ||

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

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

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

19.23.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 28400 | Extend wff notation to include the 'greater than or equal to' relation, see df-gte 28402. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |