Home | Metamath
Proof ExplorerTheorem List
(p. 282 of 325)
| < 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-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |

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

Statement | ||

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

USGrph FriendGrph | ||

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

FriendGrph | ||

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

USGrph | ||

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

USGrph | ||

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

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

USGrph | ||

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

FriendGrph | ||

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

FriendGrph | ||

Theorem | 1to3vfriswmgra 28111* | 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 28112* | 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 28113* | 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 28114* | 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 28115* | 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 28116* | 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 28117* | 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 28118* | 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 28119* | 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 28120 | 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 28121* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

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

USGrph FriendGrph | ||

Theorem | frgranbnb 28124 | 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 28125 | 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 28126 | 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 28127 | 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 28128 | 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 28129 | 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 28130 | 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 28131 | 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 28132 | 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 28133* | Lemma 1 for frgrancvvdeq 28145. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

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

Neighbors Neighbors FriendGrph | ||

Theorem | frgrancvvdeqlemA 28140* | Lemma A for frgrancvvdeq 28145. 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 28141* | Lemma B for frgrancvvdeq 28145. 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 28142* | Lemma C for frgrancvvdeq 28145. 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 28143* | Lemma 8 for frgrancvvdeq 28145. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |

Neighbors Neighbors FriendGrph | ||

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

FriendGrph Neighbors Neighbors Neighbors | ||

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

VDeg FriendGrph | ||

Theorem | frgrawopreglem2 28148* | Lemma 2 for frgrawopreg 28152. 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 28149* | Lemma 3 for frgrawopreg 28152. 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 28150* | Lemma 4 for frgrawopreg 28152. 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 28151* | Lemma 5 for frgrawopreg 28152. 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 28152* | 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 28153* | 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 28154* | 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 28155* | 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 28156* | 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 28157* | 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 28158* | 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 28159 | 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 28160 | 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 28161 | 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 28162 | 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 28163 | 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 28164* | 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 28165* | 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 28166 | 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 28167 | 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 28168* | 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 28169* | 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 28170* | 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 28171* | 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 28172* | 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 28173* | 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 28174 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13-Feb-2017.) |

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

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

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

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

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

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

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

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

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

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

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

sinh | ||

Syntax | ccosh 28188 | Extend class notation to include the hyperbolic cosine function. see df-cosh 28191. |

cosh | ||

Syntax | ctanh 28189 | Extend class notation to include the hyperbolic tangent function, see df-tanh 28192. |

tanh | ||

Definition | df-sinh 28190 | Define the hyperbolic sine function (sinh). We define it this way for cmpt 4226, which requires the form . See sinhval-named 28193 for a simple way to evaluate it. We define this function by dividing by , which uses fewer operations than many conventional definitions (and thus is more convenient to use in metamath). See sinh-conventional 28196 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.) |

sinh | ||

Definition | df-cosh 28191 | Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4226, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

Definition | df-tanh 28192 | Define the hyperbolic tangent function (tanh). We define it this way for cmpt 4226, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

tanh cosh | ||

Theorem | sinhval-named 28193 | Value of the named sinh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-sinh 28190. See sinhval 12710 for a theorem to convert this further. See sinh-conventional 28196 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.) |

sinh | ||

Theorem | coshval-named 28194 | Value of the named cosh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-cosh 28191. See coshval 12711 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

Theorem | tanhval-named 28195 | Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh 28192. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh tanh | ||

Theorem | sinh-conventional 28196 | Conventional definition of sinh. Here we show that the sinh definition we're using has the same meaning as the conventional definition used in some other sources. We choose a slightly different definition of sinh because it has fewer operations, and thus is more convenient to manipulate using metamath. (Contributed by David A. Wheeler, 10-May-2015.) |

sinh | ||

Theorem | sinhpcosh 28197 | Prove that sinh cosh using the conventional hyperbolic trig functions. (Contributed by David A. Wheeler, 27-May-2015.) |

sinh cosh | ||

19.23.4 Reciprocal trig functions (sec, csc,
cot)Define the traditional reciprocal trigonometric functions secant (sec), cosecant (csc), and cotangent (cos), along with various identities involving them. | ||

Syntax | csec 28198 | Extend class notation to include the secant function, see df-sec 28201. |

Syntax | ccsc 28199 | Extend class notation to include the cosecant function, see df-csc 28202. |

Syntax | ccot 28200 | Extend class notation to include the cotangent function, see df-cot 28203. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |