| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 645 B |
|
Quelle vect_deriv_2D.pvs Sprache: PVS |
|||||||||
|
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.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28