Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
Properties of the Trigonometric Function

Takashi Mitsuishi

Shinshu University, Nagano

Yuguang Yang

Shinshu University, Nagano
Summary.

This article introduces the monotone increasing and the monotone decreasing of
{\em sinus}
and {\em cosine}, and definitions of hyperbolic {\em sinus}, hyperbolic
{\em cosine} and
hyperbolic {\em tangent}, and some related formulas about them.
The terminology and notation used in this paper have been
introduced in the following articles
[9]
[12]
[1]
[10]
[2]
[13]
[6]
[7]
[11]
[5]
[8]
[4]
[14]
[3]

Monotone Increasing and Monotone Decreasing of Sinus and Cosine

Hyperbolic Sinus, Hyperbolic Cosine and Hyperbolic Tangent
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Jaroslaw Kotowicz.
Real sequences and basic operations on them.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Jaroslaw Kotowicz.
Properties of real functions.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Konrad Raczkowski.
Integer and rational exponents.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Konrad Raczkowski and Pawel Sadowski.
Real function continuity.
Journal of Formalized Mathematics,
2, 1990.
 [7]
Konrad Raczkowski and Pawel Sadowski.
Real function differentiability.
Journal of Formalized Mathematics,
2, 1990.
 [8]
Konrad Raczkowski and Pawel Sadowski.
Topological properties of subsets in real numbers.
Journal of Formalized Mathematics,
2, 1990.
 [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [10]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [11]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [13]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [14]
Yuguang Yang and Yasunari Shidama.
Trigonometric functions and existence of circle ratio.
Journal of Formalized Mathematics,
10, 1998.
Received March 13, 1999
[
Download a postscript version,
MML identifier index,
Mizar home page]