derivatives_alt [ T : TYPE FROM real ] : THEORY BEGIN ASSUMING IMPORTING deriv_domain_defASSUMPTION deriv_domain?[T]ASSUMPTION not_one_element?[T]ENDASSUMING IMPORTING derivatives, continuous_functions_propsVAR [T -> real]VAR TVAR real%-------------------------------------------- % Equivalent definitions of differentiation %-------------------------------------------- LEMMA (derivable?(f, x) AND deriv(f, x) = D) IFF convergence(NQ(f, x), 0, D)LEMMA convergence(NQ(f, x), 0, D)IFF (EXISTS (phi : [T -> real]) : convergence(phi, x, 0)AND FORALL y : f(y) - f(x) = (y - x) * (D + phi(y)))LEMMA (derivable?(f,x) AND deriv(f,x) = D) %% Lester IFF (EXISTS (psi : [T -> real]) : convergence(psi, x, D)AND FORALL y : f(y) - f(x) = (y - x) * psi(y))LEMMA (FORALL (epsi: posreal): abs(x) < epsi) IFF x = 0LEMMA convergence(NQ(f, x), 0, fp(x)) %% Butler IFF (EXISTS (HH: [(A(x)) -> real]): AND LAMBDA (h: (A(x))): (NQ(f,x)(h) - fp(x))))LEMMA convergence(NQ(f, x), 0, fp(x)) %% Butler IFF (EXISTS (HH: [(A(x)) -> real]): AND EXISTS (delta: posreal):FORALL (h: (A(x))): (abs(h) < delta) IMPLIES %------------------------------------ % f constant on [a, b] %------------------------------------ LEMMA a < c AND c < b AND FORALL x : a < x AND x < b IMPLIES f(x) = f(c))IMPLIES convergence(NQ(f, c), 0, 0)LEMMA a < c AND c < b AND FORALL x : a < x AND x < b IMPLIES f(x) = f(c))IMPLIES derivable?(f, c) AND deriv(f, c) = 0END derivatives_altquality 95%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
