|
tan_quad: THEORY
BEGIN
% A foundational theory of tan(x) for the interval [0,pi/2)
IMPORTING sincos_quad
x: VAR real_abs_lt_pi2
tan_value:[real_abs_lt_pi2->real] = inverse(atan)
tan_value_def: LEMMA tan_value(x) = sin_value(x)/cos_value(abs(x))
tan_value_0: LEMMA tan_value(0) = 0
tan_value_pi4: LEMMA tan_value(pi/4) = 1
END tan_quad
¤ Dauer der Verarbeitung: 0.18 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.
|
