|
vect_deriv_2D [ T : TYPE FROM real ] : THEORY
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING deriv_real_vect2[T]
s : VAR Vect2
a,r: VAR T
V : VAR (derivable_rv?)
detsv(s,V)(r): real =
det(s,V(r))
detsv_diff : LEMMA
derivable?(detsv(s,V))
detsvp_deriv : LEMMA
deriv(detsv(s,V))(r) = det(s,deriv_rv(V)(r))
sqvdot_diff : LEMMA
derivable?(LAMBDA(r):sqv(V(r)))
sqvdot_deriv : LEMMA
deriv(LAMBDA(r):sqv(V(r)))(r) = 2*V(r)*deriv_rv(V)(r)
END vect_deriv_2D
¤ Dauer der Verarbeitung: 0.14 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.
|
