atan_values: THEORY %------------------------------------------------------------------------------ % % Rick Butler NASA Langley % %------------------------------------------------------------------------------ BEGIN
IMPORTING atan, trig_values, trig_inverses
atan0 : LEMMA atan(0) = 0 %% atan_0 already used
atan1 : LEMMA atan(1) = pi/4 %% atan_1 already used
atan_1sqrt3 : LEMMA atan(1/sqrt(3)) = pi/6
atan_sqrt3 : LEMMA atan(sqrt(3)) = pi/3
atan_m1sqrt3 : LEMMA atan(-1/sqrt(3)) = -pi/6
atan_msqrt3 : LEMMA atan(-sqrt(3)) = -pi/3
x: VAR real
atan_gt_0 : LEMMA atan(x) > 0 IFF x > 0
END atan_values
¤ 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.0.1Bemerkung:
(vorverarbeitet)
¤
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.
