|
trig_ineq: THEORY
BEGIN
IMPORTING trig_basic
a,b : VAR real
n : VAR int
% ------------------- Sign of sin, cos, and tan -----------------------
cos_gt_0 : LEMMA -pi/2 < a AND a < pi/2 IMPLIES cos(a) > 0
sin_gt_0 : LEMMA 0 < a AND a < pi IMPLIES sin(a) > 0
sin_ge_0 : LEMMA 0 <= a AND a <= pi IMPLIES sin(a) >= 0
cos_ge_0 : LEMMA -pi/2 <= a AND a <= pi/2 IMPLIES cos(a) >= 0
sin_lt_0 : LEMMA pi < a AND a < 2*pi IMPLIES sin(a) < 0
cos_lt_0 : LEMMA pi/2 < a AND a < 3*pi/2 IMPLIES cos(a) < 0
sin_le_0 : LEMMA pi <= a AND a <= 2*pi IMPLIES sin(a) <= 0
cos_le_0 : LEMMA pi/2 <= a AND a <= 3*pi/2 IMPLIES cos(a) <= 0
tan_gt_0 : LEMMA 0 < a AND a < pi/2 IMPLIES tan(a) > 0
tan_lt_0 : LEMMA -pi/2 < a AND a < 0 IMPLIES tan(a) < 0
tan_pi2_def : LEMMA -pi/2 < a AND a < pi/2 IMPLIES Tan?(a)
tan_npi_def : LEMMA Tan?(n*pi)
cos_ge_0_3pi2 : LEMMA 3*pi/2 <= a AND a <= 2*pi IMPLIES cos(a) >= 0
% -------------------- Strict Inequalities --------------------
sin_increasing_imp : LEMMA
a <= pi/2 AND a >= -pi/2 AND
b <= pi/2 AND b >= -pi/2 AND
a > b
=>
sin(a) > sin(b)
sin_increasing : LEMMA
a <= pi/2 AND a >= -pi/2 AND
b <= pi/2 AND b >= -pi/2 IMPLIES
(sin(a) > sin(b)
<=>
a > b)
sin_decreasing : LEMMA
a <= 3*pi/2 AND a >= pi/2 AND
b <= 3*pi/2 AND b >= pi/2 IMPLIES
(sin(b) > sin(a)
<=>
a > b)
cos_increasing : LEMMA
a >= pi AND a <= 2*pi AND
b >= pi AND b <= 2*pi IMPLIES
(cos(a) > cos(b)
<=>
a > b)
cos_decreasing : LEMMA
a <= pi AND a >= 0 AND
b <= pi AND b >= 0 IMPLIES
(cos(b) > cos(a)
<=>
a > b)
tan_increasing_imp: LEMMA
-pi/2 < a AND a < pi/2 AND
-pi/2 < b AND b < pi/2 AND
a > b IMPLIES
tan(a) > tan(b)
tan_increasing : LEMMA
-pi/2 < a AND a < pi/2 AND
-pi/2 < b AND b < pi/2 IMPLIES
(tan(a) > tan(b) <=> a > b)
% -------------------- Non-Strict Inequalities --------------------
sin_incr : LEMMA a <= pi/2 AND a >= -pi/2 AND
b <= pi/2 AND b >= -pi/2 IMPLIES
(sin(a) >= sin(b) <=> a >= b)
sin_decr : LEMMA a <= 3*pi/2 AND a >= pi/2 AND
b <= 3*pi/2 AND b >= pi/2 IMPLIES
(sin(b) >= sin(a) <=> a >= b)
cos_incr : LEMMA a >= pi AND a <= 2*pi AND
b >= pi AND b <= 2*pi IMPLIES
(cos(a) >= cos(b) <=> a >= b)
cos_decr : LEMMA a <= pi AND a >= 0 AND
b <= pi AND b >= 0 IMPLIES
(cos(b) >= cos(a) <=> a >= b)
tan_incr : LEMMA -pi/2 < a AND a < pi/2 AND
-pi/2 < b AND b < pi/2 IMPLIES
(tan(a) >= tan(b) <=> a >= b)
% -------------------- Some properties about sin --------------------
sin_gt : LEMMA
-pi/2 <= a AND a < 3*pi/2 AND
-pi/2 <= b AND b <= pi/2 IMPLIES
(sin(a) > sin(b) IFF b < a AND a < pi-b)
sin_lt : LEMMA
-pi/2 <= a AND a < 3*pi/2 AND
-pi/2 <= b AND b <= pi/2 IMPLIES
(sin(a) < sin(b) IFF b > a OR a > pi-b)
sin_ge : LEMMA
-pi/2 <= a AND a < 3*pi/2 AND
-pi/2 <= b AND b <= pi/2 IMPLIES
(sin(a) >= sin(b) IFF b <= a AND a <= pi-b)
END trig_ineq
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
