|
vectors_2D_cos: THEORY
BEGIN
%
% .
% / \
% / \
% / \
% / \
% vc / \
% / \ vb
% / \
% / \
% / \
% / \
% / ab \
% / \
% ------------------------------------
% va
% trig: LIBRARY = "../trig"
IMPORTING vectors_2D, trig@trig_basic
va,vb,vc,v0,v1,v2: VAR Vect2
ab: VAR real
cosines_law : LEMMA
LET a = norm(va),
b = norm(vb),
c = norm(vc)
IN
vc = va - vb AND
a*b*cos(ab) = va*vb
IMPLIES
sq(c) = sq(a) + sq(b) - 2*a*b*cos(ab)
IMPORTING trig@trig_inverses
angle_exists: LEMMA (EXISTS ab: LET a = norm(va),
b = norm(vb) IN
a*b*cos(ab) = va*vb)
angle_between(u,v:Nz_vect2): real = arccos(u*v/(norm(u)*norm(v)))
cosines_law_bnd : LEMMA
LET a = norm(va),
b = norm(vb),
c = norm(vc)
IN
vc = va - vb IMPLIES
sq(c) >= sq(a-b)
cosines_law_ge : LEMMA
LET a = norm(va),
b = norm(vb),
c = norm(vc)
IN
vc = va - vb IMPLIES
c >= abs(a-b)
cosines_law_le : LEMMA
LET a = norm(va),
b = norm(vb),
c = norm(vc)
IN
vc = va - vb IMPLIES
c <= a + b
END vectors_2D_cos
¤ Dauer der Verarbeitung: 0.1 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.
|
