|
atan2_props: THEORY
BEGIN
IMPORTING atan2, trig_ineq
atan2_is_0: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
atan2(x,y) = 0 IFF (x > 0 AND y = 0)
atan2_is_pi2: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
atan2(x,y) = pi/2 IFF (x = 0 AND y > 0)
atan2_is_pi: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
atan2(x,y) = pi IFF (x < 0 AND y = 0)
atan2_is_3pi2: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
atan2(x,y) = 3*pi/2 IFF (x = 0 AND y < 0)
atan2_quad1: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
(0 < atan2(x,y) AND atan2(x,y) < pi/2) IFF
(x > 0 AND y > 0)
atan2_quad2: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
(pi/2 < atan2(x,y) AND atan2(x,y) < pi) IFF
(x < 0 AND y > 0)
atan2_quad3: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
(pi < atan2(x,y) AND atan2(x,y) < 3*pi/2) IFF
(x < 0 AND y < 0)
atan2_quad4: LEMMA FORALL (x:real,y:{z:real | x = 0 => z/=0}):
(3*pi/2 < atan2(x,y) AND atan2(x,y) < 2*pi) IFF
(x > 0 AND y < 0)
%% ------------ atan2 values -------------------------------------
IMPORTING trig_values, atan_values
nzx: VAR nzreal
atan2_0x : LEMMA atan2(0,nzx) = IF nzx > 0 THEN pi/2 ELSE 3*pi/2 ENDIF
atan2_x0 : LEMMA atan2(nzx,0) = IF nzx > 0 THEN 0 ELSE pi ENDIF
atan2_11 : LEMMA atan2(1,1) = pi/4
atan2_m11 : LEMMA atan2(-1,1) = 3*pi/4
atan2_1m1 : LEMMA atan2(1,-1) = 7*pi/4
atan2_m1m1 : LEMMA atan2(-1,-1) = 5*pi/4
atan2_1sqrt3 : LEMMA atan2(1,sqrt(3)) = pi/3
atan2_sqrt3 : LEMMA atan2(sqrt(3),1) = pi/6
atan2_m1sqrt3 : LEMMA atan2(-1,sqrt(3)) = 2*pi/3
atan2_sqrt3m1 : LEMMA atan2(sqrt(3),-1) = 11*pi/6
END atan2_props
¤ 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.
|
