|
trig_degree : THEORY
%-----------------------------------------------------------------------------
% trig_degree
% -----------
% - trig functions that take arguments in degrees: sind, cosd
% - defines conversions toRad, toDeg
%
% CHANGES
% - SIN_pos and COS_pos renamed sind_bound and cosd_bound
%-----------------------------------------------------------------------------
BEGIN
IMPORTING trig_basic,trig_approx,trig_ineq
a : VAR real
n : VAR posnat
toRad(a) : real = a*pi/180
toDeg(a) : real = a*180/pi
rad_deg : LEMMA toRad(toDeg(a)) = a
deg_rad : LEMMA toDeg(toRad(a)) = a
sind(a) : real = sin(toRad(a))
cosd(a) : real = cos(toRad(a))
tand(a:real|Tan?(toRad(a))) : real = tan(toRad(a))
sq_sin_cos_d_one : LEMMA sq(sind(a)) + sq(cosd(a)) = 1
sind_bounds : LEMMA 0 <= a AND a <= 90 IMPLIES
sind(a) >= sin_lb(a*pi_lb/180,n)
cosd_bounds : LEMMA 0 <= a AND a <= 90 IMPLIES
cosd(a) <= cos_ub(a*pi_lb/180,n)
END trig_degree
¤ Dauer der Verarbeitung: 0.17 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.
|
