Home | Metamath
Proof ExplorerTheorem List
(p. 285 of 328)
| < 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-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |

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

Statement | ||

Theorem | constr3pthlem1 28401 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |

..^ | ||

Theorem | constr3pthlem2 28402 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |

..^ | ||

Theorem | constr3pthlem3 28403 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |

..^ | ||

Theorem | constr3cycllem1 28404 | Lemma for constr3cycl 28407. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |

Theorem | constr3trl 28405 | Construction of a trail from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |

USGrph Trails | ||

Theorem | constr3pth 28406 | Construction of a path from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |

USGrph Paths | ||

Theorem | constr3cycl 28407 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |

USGrph Cycles | ||

Theorem | constr3cyclp 28408 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) |

USGrph Cycles | ||

Theorem | constr3cyclpe 28409* | If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) |

USGrph Cycles | ||

Theorem | 3v3e3cycl2 28410* | If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph. (Contributed by Alexander van der Vekens, 14-Nov-2017.) |

USGrph Cycles | ||

Theorem | 3v3e3cycl 28411* | If and only if there is a 3-cycle in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) |

USGrph Cycles | ||

Theorem | 4cycl4v4e 28412* | If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |

Cycles | ||

Theorem | 4cycl4dv 28413 | In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |

USGrph Word | ||

Theorem | 4cycl4dv4e 28414* | If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |

USGrph Cycles | ||

18.23.3.15 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 28416 as special undirected simple graphs without loops (see frisusgra 28419) and the proofs of the friendship theorem for small graphs (with up to 3 vertices), see 1to3vfriendship 28432. 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 28416, a graph without vertices is a friendship graph (see frgra0 28421), but the friendship condition does not hold (because of , see rex0 3481). Further results of this sections are: Any graph with exactly one vertex is a friendship graph, see frgra1v 28422, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 28423, 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 28426, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 28431 (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 28434 and n4cyclfrgra 28440 (these theorems correspond to Proposition 1 of [MertziosUnger] p. 153.). | ||

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

FriendGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph USGrph | ||

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

FriendGrph | ||

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

USGrph FriendGrph | ||

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

FriendGrph | ||

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

USGrph | ||

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

USGrph | ||

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

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

USGrph | ||

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

FriendGrph | ||

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

FriendGrph | ||

Theorem | 1to3vfriswmgra 28431* | 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 28432* | 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 28433* | 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 28434* | 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 | 3cyclfrgrarn1 28435* | 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 28436* | 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 | 3cyclfrgra 28437* | 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 28438 | 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 28439* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |

Theorem | n4cyclfrgra 28440 | 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 | ||

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

18.24.1 Natural deduction | ||

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

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

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

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

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

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

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

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

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

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

18.24.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 28454 | Extend class notation to include the hyperbolic sine function, see df-sinh 28457. |

sinh | ||

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

cosh | ||

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

tanh | ||

Definition | df-sinh 28457 | Define the hyperbolic sine function (sinh). We define it this way for cmpt 4093, which requires the form . See sinhval-named 28460 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 28463 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 28458 | Define the hyperbolic cosine function (cosh). We define it this way for cmpt 4093, which requires the form . (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

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

tanh cosh | ||

Theorem | sinhval-named 28460 | 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 28457. See sinhval 12450 for a theorem to convert this further. See sinh-conventional 28463 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 28461 | 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 28458. See coshval 12451 for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh | ||

Theorem | tanhval-named 28462 | 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 28459. (Contributed by David A. Wheeler, 10-May-2015.) |

cosh tanh | ||

Theorem | sinh-conventional 28463 | 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 28464 | Prove that sinh cosh using the conventional hyperbolic trig functions. (Contributed by David A. Wheeler, 27-May-2015.) |

sinh cosh | ||

18.24.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 28465 | Extend class notation to include the secant function, see df-sec 28468. |

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

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

Definition | df-sec 28468* | Define the secant function. We define it this way for cmpt 4093, which requires the form . The sec function is defined in ISO 80000-2:2009(E) operation 2-13.6 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.) |

Definition | df-csc 28469* | Define the cosecant function. We define it this way for cmpt 4093, which requires the form . The csc function is defined in ISO 80000-2:2009(E) operation 2-13.7 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.) |

Definition | df-cot 28470* | Define the cotangent function. We define it this way for cmpt 4093, which requires the form . The cot function is defined in ISO 80000-2:2009(E) operation 2-13.5 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | secval 28471 | Value of the secant function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cscval 28472 | Value of the cosecant function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cotval 28473 | Value of the cotangent function. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | seccl 28474 | The closure of the secant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | csccl 28475 | The closure of the cosecant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | cotcl 28476 | The closure of the cotangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | reseccl 28477 | The closure of the secant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recsccl 28478 | The closure of the cosecant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recotcl 28479 | The closure of the cotangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |

Theorem | recsec 28480 | The reciprocal of secant is cosine. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | reccsc 28481 | The reciprocal of cosecant is sine. (Contributed by David A. Wheeler, 14-Mar-2014.) |

Theorem | reccot 28482 | The reciprocal of cotangent is tangent. (Contributed by David A. Wheeler, 21-Mar-2014.) |

Theorem | rectan 28483 | The reciprocal of tangent is cotangent. (Contributed by David A. Wheeler, 21-Mar-2014.) |

Theorem | sec0 28484 | The value of the secant function at zero is one. (Contributed by David A. Wheeler, 16-Mar-2014.) |

Theorem | onetansqsecsq 28485 | Prove the tangent squared secant squared identity A ) ^ 2 ) ) = ( ( sec . (Contributed by David A. Wheeler, 25-May-2015.) |

Theorem | cotsqcscsq 28486 | Prove the tangent squared cosecant squared identity A ) ^ 2 ) ) = ( ( csc . (Contributed by David A. Wheeler, 27-May-2015.) |

18.24.5 Identities for "if"Utility theorems for "if". | ||

Theorem | ifnmfalse 28487 | If A is not a member of B, but an "if" condition requires it, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs vs. applying iffalse 3585 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.) |

18.24.6 Not-member-of | ||

Theorem | AnelBC 28488 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using . (Contributed by David A. Wheeler, 10-May-2015.) |

18.24.7 Decimal pointDefine the decimal point operator and the decimal fraction constructor. This can model traditional decimal point notation, and serve as a convenient way to write some fractional numbers. See df-dp 28492 and df-dp2 28491 for more information; ~? dfpval provides a more convenient way to obtain a value. This is intentionally similar to df-dec 10141. TODO: Fix non-existent label dfpval. | ||

Syntax | cdp2 28489 | Constant used for decimal fraction constructor. See df-dp2 28491. |

_ | ||

Syntax | cdp 28490 | Decimal point operator. See df-dp 28492. |

Definition | df-dp2 28491 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 10141. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Definition | df-dp 28492* |
Define the (decimal point) operator. For example,
, and
;__ ;;;; ;;;
Unary minus, if applied, should normally be applied in front of the
parentheses.
Metamath intentionally does not have a built-in construct for numbers, so it can show that numbers are something you can build based on set theory. However, that means that metamath has no built-in way to handle decimal numbers as traditionally written, e.g., "2.54", and its parsing system intentionally does not include the complexities necessary to define such a parsing system. Here we create a system for modeling traditional decimal point notation; it is not syntactically identical, but it is sufficiently similar so it is a reasonable model of decimal point notation. It should also serve as a convenient way to write some fractional numbers. The RHS is , not ; this should simplify some proofs. The LHS is , since that is what is used in practice. The definition intentionally does not allow negative numbers on the LHS; if it did, nonzero fractions would produce the wrong results. (It would be possible to define the decimal point to do this, but using it would be more complicated, and the expression is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dp2cl 28493 | Define the closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dpval 28494 | Define the value of the decimal point operator. See df-dp 28492. (Contributed by David A. Wheeler, 15-May-2015.) |

_ | ||

Theorem | dpcl 28495 | Prove that the closure of the decimal point is as we have defined it. See df-dp 28492. (Contributed by David A. Wheeler, 15-May-2015.) |

Theorem | dpfrac1 28496 | Prove a simple equivalence involving the decimal point. See df-dp 28492 and dpcl 28495. (Contributed by David A. Wheeler, 15-May-2015.) |

; | ||

18.24.8 Signum (sgn or sign)
function | ||

Syntax | csgn 28497 | Extend class notation to include the Signum function. |

sgn | ||

Definition | df-sgn 28498 | Signum function. Pronounced "signum" , otherwise it might be confused with "sine". Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. We define this over (df-xr 8887) instead of so that it can accept and . Note that df-psgn 27518 defines the sign of a permutation, which is different. Value shown in sgnval 28499. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgnval 28499 | Value of Signum function. Pronounced "signum" . See df-sgn 28498. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn | ||

Theorem | sgn0 28500 | Proof that signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |

sgn |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |