|
trig_props: THEORY
BEGIN
% analysis: LIBRARY "../analysis"
IMPORTING power_series_deriv[real],
trig_fun, analysis@derivative_props, analysis@deriv_domain
n: VAR nat
x: VAR real
sin_derivable: LEMMA derivable?(sin);
deriv_sin : THEOREM deriv(sin)(x) = cos(x)
cos_derivable: LEMMA derivable?(cos);
deriv_cos : THEOREM deriv(cos)(x) = -sin(x)
sin2_cos2_derivable: LEMMA derivable?(sin*sin+cos*cos)
sin2_cos2 : THEOREM sin*sin + cos*cos = const_fun(1)
sin_cos_one : THEOREM sin(x)*sin(x) + cos(x)*cos(x) = 1
sin_lt_1 : LEMMA abs(sin(x)) <= 1
END trig_props
¤ Dauer der Verarbeitung: 0.14 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.
|
