Home | Metamath
Proof Explorer Theorem List (p. 272 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eulerpath 27101* | A pseudograph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
Vtx UPGraph EulerPaths VtxDeg | ||
Theorem | eulercrct 27102* | A pseudograph with an Eulerian circuit (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021.) |
Vtx UPGraph EulerPaths Circuits VtxDeg | ||
Theorem | eucrctshift 27103* | Cyclically shifting the indices of an Eulerian circuit results in an Eulerian circuit . (Contributed by AV, 15-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Vtx iEdg Circuits ..^ cyclShift EulerPaths EulerPaths Circuits | ||
Theorem | eucrct2eupth1 27104 | Removing one edge from a nonempty graph with an Eulerian circuit results in a graph with an Eulerian path . This is the special case of eucrct2eupth 27105 (with ) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021.) |
Vtx iEdg EulerPaths Circuits Vtx iEdg ..^ ..^ EulerPaths | ||
Theorem | eucrct2eupth 27105* | Removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path . (Contributed by AV, 17-Mar-2021.) |
Vtx iEdg EulerPaths Circuits Vtx ..^ iEdg ..^ cyclShift ..^ ..^ EulerPaths | ||
According to Wikipedia ("Seven Bridges of Königsberg", 9-Mar-2021, https://en.wikipedia.org/wiki/Seven_Bridges_of_Koenigsberg): "The Seven Bridges of Königsberg is a historically notable problem in mathematics. Its negative resolution by Leonhard Euler in 1736 laid the foundations of graph theory and prefigured the idea of topology. The city of Königsberg in [East] Prussia (now Kaliningrad, Russia) was set on both sides of the Pregel River, and included two large islands - Kneiphof and Lomse - which were connected to each other, or to the two mainland portions of the city, by seven bridges. The problem was to devise a walk through the city that would cross each of those bridges once and only once.". Euler proved that the problem has no solution by applying Euler's theorem to the Königsberg graph, which is obtained by replacing each land mass with an abstract "vertex" or node, and each bridge with an abstract connection, an "edge", which connects two land masses/vertices. The Königsberg graph is a multigraph consisting of 4 vertices and 7 edges, represented by the following ordered pair: , see konigsbergumgr 27112. konigsberg 27119 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution. | ||
Theorem | konigsbergvtx 27106 | The set of vertices of the Königsberg graph . (Contributed by AV, 28-Feb-2021.) |
Vtx | ||
Theorem | konigsbergiedg 27107 | The indexed edges of the Königsberg graph . (Contributed by AV, 28-Feb-2021.) |
iEdg | ||
Theorem | konigsbergiedgw 27108* | The indexed edges of the Königsberg graph is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
Word | ||
Theorem | konigsbergiedgwOLD 27109* | The indexed edges of the Königsberg graph is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) Obsolete version of konigsbergiedgw 27108 as of 9-Mar-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Word | ||
Theorem | konigsbergssiedgwpr 27110* | Each subset of the indexed edges of the Königsberg graph is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
Word Word ++ Word | ||
Theorem | konigsbergssiedgw 27111* | Each subset of the indexed edges of the Königsberg graph is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
Word Word ++ Word | ||
Theorem | konigsbergumgr 27112 | The Königsberg graph is a multigraph. (Contributed by AV, 28-Feb-2021.) (Revised by AV, 9-Mar-2021.) |
UMGraph | ||
Theorem | konigsbergupgrOLD 27113 | The Königsberg graph is a pseudograph. (Contributed by AV, 28-Feb-2021.) Obsolete version of konigsbergumgr 27112 as of 9-Mar-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
UPGraph | ||
Theorem | konigsberglem1 27114 | Lemma 1 for konigsberg 27119: Vertex has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
VtxDeg | ||
Theorem | konigsberglem2 27115 | Lemma 2 for konigsberg 27119: Vertex has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
VtxDeg | ||
Theorem | konigsberglem3 27116 | Lemma 3 for konigsberg 27119: Vertex has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
VtxDeg | ||
Theorem | konigsberglem4 27117* | Lemma 4 for konigsberg 27119: Vertices are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
VtxDeg | ||
Theorem | konigsberglem5 27118* | Lemma 5 for konigsberg 27119: The set of vertices of odd degree is greater than 2. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
VtxDeg | ||
Theorem | konigsberg 27119 | The Königsberg Bridge problem. If is the Königsberg graph, i.e. a graph on four vertices , with edges , then vertices each have degree three, and has degree five, so there are four vertices of odd degree and thus by eulerpath 27101 the graph cannot have an Eulerian path. It is sufficient to show that there are 3 vertices of odd degree, since a graph having an Eulerian path can only have 0 or 2 vertices of odd degree. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 9-Mar-2021.) |
EulerPaths | ||
Syntax | cfrgr 27120 | Extend class notation with friendship graphs. |
FriendGraph | ||
Definition | df-frgr 27121* | Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called the friendship condition , see definition in [MertziosUnger] p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
FriendGraph USGraph Vtx Edg | ||
Theorem | isfrgr 27122* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg FriendGraph USGraph | ||
Theorem | frgrusgrfrcond 27123* | A friendship graph is a simple graph which fulfils the friendship condition. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg FriendGraph USGraph | ||
Theorem | frgrusgr 27124 | A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
FriendGraph USGraph | ||
Theorem | frgr0v 27125 | Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx FriendGraph iEdg | ||
Theorem | frgr0vb 27126 | Any null graph (without vertices and edges) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx iEdg FriendGraph | ||
Theorem | frgruhgr0v 27127 | Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
UHGraph Vtx FriendGraph | ||
Theorem | frgr0 27128 | The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
FriendGraph | ||
Theorem | rspc2vd 27129* | Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class for the second set variable may depend on the first set variable . (Contributed by AV, 29-Mar-2021.) |
Theorem | frcond1 27130* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | frcond2 27131* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | frgreu 27132* | Variant of frcond2 27131: Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
Vtx Edg FriendGraph | ||
Theorem | frcond3 27133* | The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 30-Dec-2021.) |
Vtx Edg FriendGraph NeighbVtx NeighbVtx | ||
Theorem | frcond4 27134* | The friendship condition, alternatively expressed by neighborhoods: 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.) (Revised by AV, 29-Mar-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg FriendGraph NeighbVtx NeighbVtx | ||
Theorem | frgr1v 27135 | Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
USGraph Vtx FriendGraph | ||
Theorem | nfrgr2v 27136 | Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Proof shortened by Alexander van der Vekens, 13-Sep-2018.) (Revised by AV, 29-Mar-2021.) |
Vtx FriendGraph | ||
Theorem | frgr3vlem1 27137* | Lemma 1 for frgr3v 27139. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg USGraph | ||
Theorem | frgr3vlem2 27138* | Lemma 2 for frgr3v 27139. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg USGraph | ||
Theorem | frgr3v 27139 | 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.) (Revised by AV, 29-Mar-2021.) |
Vtx Edg USGraph FriendGraph | ||
Theorem | 1vwmgr 27140* | Every graph with one vertex (which may be connect with itself by (multiple) loops!) is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
Theorem | 3vfriswmgrlem 27141* | Lemma for 3vfriswmgr 27142. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
Vtx Edg USGraph | ||
Theorem | 3vfriswmgr 27142* | Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 1to2vfriswmgr 27143* | Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 1to3vfriswmgr 27144* | Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 1to3vfriendship 27145* | 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.) (Revised by AV, 31-Mar-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 2pthfrgrrn 27146* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) 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.) (Revised by AV, 1-Apr-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 2pthfrgrrn2 27147* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) 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.) (Revised by AV, 1-Apr-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 2pthfrgr 27148* | Between any two (different) vertices in a friendship graph, tere is a 2-path (simple path of length 2), see Proposition 1(b) 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.) (Revised by AV, 1-Apr-2021.) |
Vtx FriendGraph SPathsOn | ||
Theorem | 3cyclfrgrrn1 27149* | 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.) (Revised by AV, 2-Apr-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 3cyclfrgrrn 27150* | 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.) (Revised by AV, 2-Apr-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 3cyclfrgrrn2 27151* | 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.) (Revised by AV, 2-Apr-2021.) |
Vtx Edg FriendGraph | ||
Theorem | 3cyclfrgr 27152* | 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.) (Revised by AV, 2-Apr-2021.) |
Vtx FriendGraph Cycles | ||
Theorem | 4cycl2v2nb 27153 | In a (maybe degenerated) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
Theorem | 4cycl2vnunb 27154* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
Theorem | n4cyclfrgr 27155 | There is no 4-cycle in a friendship graph, see Proposition 1(a) of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
FriendGraph Cycles | ||
Theorem | 4cyclusnfrgr 27156 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
Vtx Edg USGraph FriendGraph | ||
Theorem | frgrnbnb 27157 | If two neighbors and of a vertex have a common neighbor in a friendship graph, then this common neighbor must be the vertex . (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
Edg NeighbVtx FriendGraph | ||
Theorem | frgrconngr 27158 | A friendship graph is connected, see remark 1 in [MertziosUnger] p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 1-Apr-2021.) |
FriendGraph ConnGraph | ||
Theorem | vdgn0frgrv2 27159 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
Vtx FriendGraph VtxDeg | ||
Theorem | vdgn1frgrv2 27160 | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
Vtx FriendGraph VtxDeg | ||
Theorem | vdgn1frgrv3 27161* | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 4-Apr-2021.) |
Vtx FriendGraph VtxDeg | ||
Theorem | vdgfrgrgt2 27162 | 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 remark 3 in [MertziosUnger] p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 5-Apr-2021.) |
Vtx FriendGraph VtxDeg | ||
In this section, the friendship theorem friendship 27257 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 27173, frgrregorufr 27189 and frrusgrord0 27204) and additional statements (numbered in the order of their occurence in the paper) in Huneke's proof are cited in the corresponding theorems. | ||
Theorem | frgrncvvdeqlem1 27163 | Lemma 1 for frgrncvvdeq 27173. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 8-May-2021.) (Proof shortened by AV, 28-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem2 27164* | Lemma 2 for frgrncvvdeq 27173. In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem3 27165* | Lemma 3 for frgrncvvdeq 27173. The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph NeighbVtx | ||
Theorem | frgrncvvdeqlem4 27166* | Lemma 4 for frgrncvvdeq 27173. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem5 27167* | Lemma 5 for frgrncvvdeq 27173. 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.) (Revised by AV, 10-May-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph NeighbVtx | ||
Theorem | frgrncvvdeqlem6 27168* | Lemma 6 for frgrncvvdeq 27173. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem7 27169* | Lemma 7 for frgrncvvdeq 27173. This corresponds to statement 1 in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem8 27170* | Lemma 8 for frgrncvvdeq 27173. This corresponds to statement 2 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.) (Revised by AV, 10-May-2021.) (Revised by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem9 27171* | Lemma 9 for frgrncvvdeq 27173. This corresponds to statement 3 in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeqlem10 27172* | Lemma 10 for frgrncvvdeq 27173. (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
Vtx Edg NeighbVtx NeighbVtx FriendGraph | ||
Theorem | frgrncvvdeq 27173* | In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 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.) (Revised by AV, 10-May-2021.) |
Vtx VtxDeg FriendGraph NeighbVtx | ||
Theorem | frgrwopreglem4a 27174 | In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 27179 without a fixed degree and without using the sets and . (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreglem5a 27175 | If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 27185 without a fixed degree and without using the sets and . (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreglem1 27176* | Lemma 1 for frgrwopreg 27187: the classes and are sets. The definition of and corresponds to definition 3 in [Huneke] p. 2: "Let A be the set of all vertices of degree k, let B be the set of all vertices of degree different from k, ..." (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.) |
Vtx VtxDeg | ||
Theorem | frgrwopreglem2 27177* | Lemma 2 for frgrwopreg 27187. If the set of vertices of degree is not empty in a friendship graph with at least two vertices, then must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 2-Jan-2022.) |
Vtx VtxDeg FriendGraph | ||
Theorem | frgrwopreglem3 27178* | Lemma 3 for frgrwopreg 27187. The vertices in the sets and have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 2-Jan-2022.) |
Vtx VtxDeg | ||
Theorem | frgrwopreglem4 27179* | Lemma 4 for frgrwopreg 27187. In a friendship graph each vertex with degree is connected with any vertex with degree other than . This corresponds to statement 4 in [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.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopregasn 27180* | According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 27182 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopregbsn 27181* | According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 27183 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreg1 27182* | According to statement 5 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.) (Proof shortened by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreg2 27183* | According to statement 5 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.) (Proof shortened by AV, 4-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreglem5lem 27184* | Lemma for frgrwopreglem5 27185. (Contributed by AV, 5-Feb-2022.) |
Vtx VtxDeg Edg | ||
Theorem | frgrwopreglem5 27185* | Lemma 5 for frgrwopreg 27187. If as well as contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in [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.) (Proof shortened by AV, 5-Feb-2022.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreglem5ALT 27186* | Alternate direct proof of frgrwopreglem5 27185, not using frgrwopreglem5a 27175. This proof would be even a little bit shorter than the proof of frgrwopreglem5 27185 without using frgrwopreglem5lem 27184. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 3-Jan-2022.) (Proof shortened by AV, 5-Feb-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
Vtx VtxDeg Edg FriendGraph | ||
Theorem | frgrwopreg 27187* | In a friendship graph there are either no vertices ( ) or exactly one vertex ( ) having degree , or all ( ) or all except one vertices ( ) have degree . (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 3-Jan-2022.) |
Vtx VtxDeg FriendGraph | ||
Theorem | frgrregorufr0 27188* | In a friendship graph there are either no vertices having degree , or all vertices have degree for any (nonnegative integer) , unless there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 11-May-2021.) (Proof shortened by AV, 3-Jan-2022.) |
Vtx Edg VtxDeg FriendGraph | ||
Theorem | frgrregorufr 27189* | If there is a vertex having degree for each (nonnegative integer) in a friendship graph, then either all vertices have degree or there is a universal friend. This corresponds to claim 2 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.) |
Vtx Edg VtxDeg FriendGraph | ||
Theorem | frgrregorufrg 27190* | If there is a vertex having degree for each nonnegative integer in a friendship graph, then there is a universal friend. This corresponds to claim 2 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". Variant of frgrregorufr 27189 with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.) |
Vtx Edg FriendGraph VtxDeg RegUSGraph | ||
Theorem | frgr2wwlkeu 27191* | 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. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
Vtx FriendGraph WWalksNOn | ||
Theorem | frgr2wwlkn0 27192 | In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) |
Vtx FriendGraph WWalksNOn | ||
Theorem | frgr2wwlk1 27193 | In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
Vtx FriendGraph WWalksNOn | ||
Theorem | frgr2wsp1 27194 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 13-May-2021.) |
Vtx FriendGraph WSPathsNOn | ||
Theorem | frgr2wwlkeqm 27195 | If there is a (simple) path of length 2 from one vertex to another vertex and a (simple) path of length 2 from the other vertex back to the first vertex in a friendship graph, then the middle vertex is the same. This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 20-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 7-Jan-2022.) |
FriendGraph WWalksNOn WWalksNOn | ||
Theorem | frgrhash2wsp 27196 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with n vertices. This corresponds to the proof of claim 3 in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, Huneke counts undirected paths, so obtains the result ( ), whereas we count directed paths, obtaining twice that number. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 10-Jan-2022.) |
Vtx FriendGraph WSPathsN | ||
Theorem | fusgreg2wsplem 27197* | Lemma for fusgreg2wsp 27200 and related theorems. (Contributed by AV, 8-Jan-2022.) |
Vtx WSPathsN WSPathsN | ||
Theorem | fusgr2wsp2nb 27198* | The set of paths of length 2 with a given vertex in the middle for a finite simple 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.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 8-Jan-2022.) |
Vtx WSPathsN FinUSGraph NeighbVtx NeighbVtx | ||
Theorem | fusgreghash2wspv 27199* | According to statement 7 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 directed simple paths of length 2 represented by length 3 strings, we have again k*(k-1) such paths, see also comment of frgrhash2wsp 27196. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 10-Jan-2022.) |
Vtx WSPathsN FinUSGraph VtxDeg | ||
Theorem | fusgreg2wsp 27200* | In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.) |
Vtx WSPathsN FinUSGraph WSPathsN |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |