Home | Metamath
Proof ExplorerTheorem List
(p. 279 of 323)
| < 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-21811) |
Hilbert Space Explorer
(21812-23334) |
Users' Mathboxes
(23335-32225) |

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

Statement | ||

Theorem | 1conngra 27801 | A class/graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |

ConnGrph | ||

Theorem | cusconngra 27802 | A complete (undirected simple) graph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |

ComplUSGrph ConnGrph | ||

19.22.3.5 Vertex DegreeThe vertext degree is currently defined in the Mathbox of Mario Carneiro as VDeg , see df-vdgr 24466. Since simple undirected graphs have no (self-)loops, the second summand will be 0, see vdusgraval 27816, simplifying the definition essentially. Although vdusgraval 27816 would hold also for infinite graphs (which can have vertices with infinite degree), we cannot derive this from the current definition, since the operation is only defined for complex numbers and not for extended real numbers containing (pnfxr 10606) which is not a real number (pnfnre 9021) and therefor also no complex number. So even for simple undirected graphs we cannot derive VDeg from (this can be a valid statement since the codomain of the function contains , see hashf 11512). However, if the addition over extended real numbers ( see df-xadd 10604) would be used within the definition of VDeg, this definition would be valid also for infinite graphs, since we can prove vdusgraval 27816 using (see xaddpnf2 10706) then. Therefore, a corresponding alternative definition is provided in the following ( see df-vdgre 27804), by which the analogon vdusgrav 27817 for vdusgraval 27816 which is also valid for infinite graphs can be proven. | ||

Syntax | cvdgr 27803 | Extend class notation with the vertex degree function. |

VDegr | ||

Definition | df-vdgre 27804* | Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Analogous to df-vdgr 24466 (definition of VDeg), but appropriate also for infinite graphs. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgrefval 27805* | The value of the vertex degree function, analogous to vdgrfval 24476. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgreval 27806* | The value of the vertex degree function, analogous to vdgrval 24477. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgref 27807 | The vertex degree function is a function from vertices to nonnegative integers or plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgrefinf 27808 | The vertex degree function on finite graphs is a function from vertices to nonnegative integers, analogous to vdgrf 24478. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgrvdgre 27809 | For finite graphs (or at least for graphs with a finite set of edges), the definitions of VDeg and VDegr are equivalent. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDeg VDegr | ||

Theorem | vdgre0 27810 | The degree of a vertex in an empty graph is zero, because there are no edges, analogous to vdgr0 24479. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

VDegr | ||

Theorem | vdgreun 27811 | The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph, analogous to vdgrun 24480. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |

UMGrph UMGrph VDegr VDegr VDegr | ||

Theorem | vdgre1d 27812 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree, analogous to vdgr1d 24481. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

VDegr | ||

Theorem | vdgre1b 27813 | The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree, analogous to vdgr1b 24482. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

VDegr | ||

Theorem | vdgre1c 27814 | The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree, analogous to vdgr1c 24483. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

VDegr | ||

Theorem | vdgre1a 27815 | The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree, analogous to vdgr1d 24481. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

VDegr | ||

Theorem | vdusgraval 27816* | The value of the vertex degree function for simple undirected graphs with a finite number of edges. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |

USGrph VDeg | ||

Theorem | vdusgrav 27817* | The value of the vertex degree function for simple undirected graphs, analogous to vdusgraval 27816. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

USGrph VDegr | ||

Theorem | vdusgra0nedg 27818* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |

USGrph VDeg | ||

Theorem | vdgrnn0pnf 27819 | The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |

USGrph VDegr | ||

Theorem | hashnbgravd 27820 | The size of the set of the neighbors of a vertex is the vertex degree of this vertex. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |

USGrph Neighbors VDeg | ||

Theorem | hashnbgravdg 27821 | The size of the set of the neighbors of a vertex is the vertex degree of this vertex, analogous to hashnbgravd 27820. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

USGrph Neighbors VDegr | ||

Theorem | usgravd0nedg 27822* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge, analogous to vdusgra0nedg 27818. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |

USGrph VDegr | ||

19.22.3.6 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 27824 as special undirected simple graphs without loops (see frisusgra 27827) and the proofs of the friendship theorem for small graphs (with up to 3 vertices), see 1to3vfriendship 27843. 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 27824, a graph without vertices is a friendship graph (see frgra0 27829), but the friendship condition does not hold (because of , see rex0 3556). Further results of this sections are: Any graph with exactly one vertex is a friendship graph, see frgra1v 27833, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 27834, 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 27837, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 27842 (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 27845 and n4cyclfrgra 27853 (these theorems correspond to Proposition 1 of [MertziosUnger] p. 153.). In addition, the first two Lemmas ("claims") in the proof of [Huneke] p. 1 are proven, see frgrancvvdgeq 27878 and frgraregorufr 27888. | ||

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

FriendGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph | ||

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

USGrph FriendGrph | ||

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

FriendGrph | ||

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

USGrph | ||

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

USGrph | ||

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

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

USGrph | ||

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

FriendGrph | ||

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

FriendGrph | ||

Theorem | 1to3vfriswmgra 27842* | 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 27843* | 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 27844* | 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 27845* | 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 27846* | 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 27847* | 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 27848* | 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 27849* | 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 27850* | 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 27851 | 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 27852* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

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

USGrph FriendGrph | ||

Theorem | frgranbnb 27855 | 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 27856 | 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 27857 | 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 27858 | 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 VDegr | ||

Theorem | vdn0frgrav2 27859 | 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 27860 | 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 VDegr | ||

Theorem | vdn1frgrav2 27861 | 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 27862 | 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 VDegr | ||

Theorem | vdfrgragt2 27863 | 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". Unfortunately, the vertex degree function is (currently) not (properly) defined for infinite graphs (at least for graphs with infinite many edges), see the comments before vdusgraval 27816. Therefore, the finiteness (at least of the number of edges) must be assumed here. However, if the definition of the vertex degree was changed so that VDeg if there are infinite many edges adjacent to the vertex , this theorem would also be valid without assuming the finiteness of the number of edges. (Contributed by Alexander van der Vekens, 11-Dec-2017.) |

FriendGrph VDeg | ||

Theorem | vdgfrgragt2 27864 | 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 VDegr | ||

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

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemA 27872* | Lemma A for frgrancvvdeq 27877. 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 27873* | Lemma B for frgrancvvdeq 27877. 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 27874* | Lemma C for frgrancvvdeq 27877. 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 27875* | Lemma 8 for frgrancvvdeq 27877. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

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

FriendGrph Neighbors Neighbors Neighbors | ||

Theorem | frgrancvvdeq 27877* | 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 27878* | 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 VDegr VDegr | ||

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

VDegr FriendGrph | ||

Theorem | frgrawopreglem2 27880* | Lemma 2 for frgrawopreg 27884. 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.) |

VDegr FriendGrph | ||

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

VDegr VDegr VDegr | ||

Theorem | frgrawopreglem4 27882* | Lemma 4 for frgrawopreg 27884. 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.) |

VDegr FriendGrph | ||

Theorem | frgrawopreglem5 27883* | Lemma 5 for frgrawopreg 27884. 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.) |

VDegr FriendGrph | ||

Theorem | frgrawopreg 27884* | 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.) |

VDegr FriendGrph | ||

Theorem | frgrawopreg1 27885* | 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.) |

VDegr FriendGrph | ||

Theorem | frgrawopreg2 27886* | 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.) |

VDegr FriendGrph | ||

Theorem | frgraregorufr0 27887* | 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 VDegr VDegr | ||

Theorem | frgraregorufr 27888* | 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 VDegr VDegr | ||

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 27889 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1752. (Contributed by DAW, 13-Feb-2017.) |

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

Theorem | sbidd-misc 27891 | An identity theorem for substitution. See sbid 1934. 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 27892 | Extend wff notation to include the 'greater than or equal to' relation, see df-gte 27894. |

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

Definition | df-gte 27894 |
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 9020.
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 27895), 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 27896 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 27895 |
The 'greater than' relation is merely the converse of the 'less than or
equal to' relation defined by df-lt 8897. Defined in ISO 80000-2:2009(E)
operation 2-7.12. See df-gte 27894 for a discussion on why this approach is
used for the definition. See gt-lt 27897 and gt-lth 27899 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 27896 | Simple relationship between and . (Contributed by David A. Wheeler, 10-May-2015.) (New usage is discouraged.) |

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

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

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

Theorem | ex-gt 27900 | 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.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |