Home | Metamath
Proof ExplorerTheorem List
(p. 283 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-22409) |
Hilbert Space Explorer
(22410-23932) |
Users' Mathboxes
(23933-32601) |

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

Statement | ||

Definition | df-2spthonot 28201* | Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt SPathOn | ||

Definition | df-2spthsot 28202* | Define the collection of all simple paths of length 2 as ordered triple. (in a graph) (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt 2SPathOnOt | ||

Theorem | el2wlkonotlem 28203 | Lemma for el2wlkonot 28210. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |

Walks | ||

Theorem | is2wlkonot 28204* | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |

2WalksOnOt WalkOn | ||

Theorem | is2spthonot 28205* | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt SPathOn | ||

Theorem | 2wlkonot 28206* | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |

2WalksOnOt WalkOn | ||

Theorem | 2spthonot 28207* | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt SPathOn | ||

Theorem | 2wlksot 28208* | The set of walks of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |

2WalksOt 2WalksOnOt | ||

Theorem | 2spthsot 28209* | The set of simple paths of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |

2SPathOnOt 2SPathOnOt | ||

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

2WalksOnOt Walks | ||

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

2SPathOnOt SPaths | ||

Theorem | el2spthonot0 28212* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |

2SPathOnOt 2SPathOnOt | ||

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

2WalksOnOt Walks | ||

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

2WalksOnOt Walks | ||

Theorem | el2wlkonotot1 28215 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |

2WalksOnOt 2WalksOnOt | ||

Theorem | 2wlkonot3v 28216 | If an ordered triple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |

2WalksOnOt | ||

Theorem | 2spthonot3v 28217 | If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt | ||

Theorem | 2wlkonotv 28218 | If an ordered tripple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |

2WalksOnOt | ||

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

2WalksOt 2WalksOnOt | ||

Theorem | el2spthsoton 28220* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |

2SPathOnOt 2SPathOnOt | ||

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

2WalksOt Walks | ||

Theorem | el2pthsot 28222* | 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 28223* | 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 28224 | 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 28225* | 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 28226 | 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 28227* | 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 28228 | 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 28229 | 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 28230 | 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 28231* | 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 28232* | 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 28233 | 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 28234* | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |

USGrph VDeg | ||

Theorem | usgfiregdegfi 28235* | 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 28237 as special undirected simple graphs without loops (see frisusgra 28240) and the proofs of the friendship theorem for small graphs (with up to 3 vertices), see 1to3vfriendship 28256. 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 28237, a graph without vertices is a friendship graph (see frgra0 28242), 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 28246, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 28247, 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 28250, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 28255 (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 28258 and n4cyclfrgra 28266 (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 28290, frgraregorufr 28300 and frgregordn0 28317. | ||

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

FriendGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph | ||

Theorem | frgraunss 28243* | 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 28244* | 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 28245* | 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 28246 | Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |

USGrph FriendGrph | ||

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

FriendGrph | ||

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

USGrph | ||

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

USGrph | ||

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

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

USGrph | ||

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

FriendGrph | ||

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

FriendGrph | ||

Theorem | 1to3vfriswmgra 28255* | 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 28256* | 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 28257* | 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 28258* | 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 28259* | 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 28260* | 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 28261* | 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 28262* | 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 28263* | 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 28264 | 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 28265* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | n4cyclfrgra 28266 | 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 28267 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |

USGrph FriendGrph | ||

Theorem | frgranbnb 28268 | 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 28269 | 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 28270 | 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 28271 | 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 28272 | 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 28273 | 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 28274 | 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 28275 | 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 28276 | 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 28277* | Lemma 1 for frgrancvvdeq 28289. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem3 28279* | Lemma 3 for frgrancvvdeq 28289. 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 28280* | Lemma 4 for frgrancvvdeq 28289. 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 28281* | Lemma 5 for frgrancvvdeq 28289. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlem6 28282* | Lemma 6 for frgrancvvdeq 28289. 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 28283* | Lemma 7 for frgrancvvdeq 28289. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemA 28284* | Lemma A for frgrancvvdeq 28289. 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 28285* | Lemma B for frgrancvvdeq 28289. 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 28286* | Lemma C for frgrancvvdeq 28289. 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 28287* | Lemma 8 for frgrancvvdeq 28289. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

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

FriendGrph Neighbors Neighbors Neighbors | ||

Theorem | frgrancvvdeq 28289* | 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 28290* | 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 28291* | Lemma 1 for frgrawopreg 28296. In a friendship graph, the classes A and B are sets. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |

VDeg FriendGrph | ||

Theorem | frgrawopreglem2 28292* | Lemma 2 for frgrawopreg 28296. 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 28293* | Lemma 3 for frgrawopreg 28296. 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 28294* | Lemma 4 for frgrawopreg 28296. 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 28295* | Lemma 5 for frgrawopreg 28296. 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 28296* | 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 28297* | 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 28298* | 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 28299* | 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 28300* | 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 |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |