|
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.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
