|
law_cos_pos_3D: THEORY
BEGIN
% v2
% .
% / \
% / \
% / \
% / \
% c / \
% / \ b
% / \
% / \
% / \
% / \
% / ab \
% / \
% ------------------------------------
% v0 a v1
IMPORTING trig@trig_basic,
distance_3D
v0,v1,v2: VAR Vect3
ab: VAR real
law_cosines : LEMMA
LET a = dist(v1,v0),
b = dist(v2,v1),
c = dist(v2,v0)
IN
a*b*cos(ab) = (v1-v0)*(v1-v2)
IMPLIES
sq(c) = sq(a) + sq(b) - 2*a*b*cos(ab)
law_cosines_alt : LEMMA
LET a = dist(v1,v0),
b = dist(v2,v1),
c = dist(v2,v0)
IN
sq(c) = sq(a) + sq(b) - 2*(v1-v0)*(v1-v2)
IMPORTING trig@trig_inverses
angle_exists: LEMMA (EXISTS ab: LET a = dist(v1,v0),
b = dist(v2,v1) IN
a*b*cos(ab) = (v1-v0)*(v1-v2))
angle_between(u,v:Nz_vect3): real = arccos(u*v/(norm(u)*norm(v)))
law_cosines_bnd : LEMMA
LET a = dist(v1,v0),
b = dist(v2,v1),
c = dist(v2,v0)
IN
sq(c) >= sq(a-b)
law_cosines_bnd_abs : LEMMA
LET a = dist(v1,v0),
b = dist(v2,v1),
c = dist(v2,v0)
IN
c >= abs(a-b)
law_cosines_le : LEMMA LET a = dist(v1,v0),
b = dist(v2,v1),
c = dist(v2,v0)
IN
c <= a + b
END law_cos_pos_3D
¤ Dauer der Verarbeitung: 0.16 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.
|
