|
horizontal_sq_dtca[D:posreal] : THEORY
BEGIN
IMPORTING vect_analysis@vect_deriv_2D[real],
tangent_line[D]
V : VAR (differentiable_rv?)
a,r : VAR real
s : VAR Vect2
ss : VAR Ss_vect2
pm : VAR Sign
horizontal_sq_dtca_diff : LEMMA
(FORALL (a):nz_vect2?(V(a))) IMPLIES
derivable?[real](LAMBDA (r: real): horizontal_sq_dtca(s, V(r)), r)
horizontal_sq_dtca_deriv : LEMMA
(FORALL (a):nz_vect2?(V(a))) IMPLIES
deriv(LAMBDA(r:real):horizontal_sq_dtca(s,V(r)),r) =
LET v = V(r),
w = deriv_rv(V)(r) IN
(2*sqv(v)*det(s,v)*det(s,w)-2*sq(det(s,v))*(v*w))/sq(sqv(v))
horizontal_sq_dtca_deriv_simpl : LEMMA
(FORALL (a):nz_vect2?(V(a))) IMPLIES
LET v = V(r),
w = deriv_rv(V)(r) IN
(2*sqv(v)*det(s,v)*det(s,w)-2*sq(det(s,v))*(v*w))/sq(sqv(v)) =
2*det(s,v)*det(V(r),w)*(s*V(r))/sq(sqv(v))
horizontal_sq_dtca_deriv_sign : LEMMA
(FORALL (a):nz_vect2?(V(a))) AND
line_solution?(ss,V(r)) IMPLIES
(pm*deriv(LAMBDA(r:real):horizontal_sq_dtca(ss,V(r)),r) > 0 IFF
LET v = V(r),
w = deriv_rv(V)(r),
eps = eps_line(ss,v) IN
pm*(Q(ss,eps)*w) > 0)
END horizontal_sq_dtca
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
