|
vectors_cos[n: posnat]: THEORY
BEGIN
%
% .
% / \
% / \
% / \
% / \
% vc / \
% / \ vb
% / \
% / \
% / \
% / \
% / ab \
% / \
% ------------------------------------
% va
IMPORTING vectors, trig@trig_basic
va,vb,vc,v0,v1,v2: VAR Vector[n]
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_vector[n]): 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_cos
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
