derivative_def: THEORY BEGIN anal: LIBRARY = "../analysis/" IMPORTING anal@derivatives[real] f: VAR [real -> real] x,L: VAR real epsilon, delta: VAR posreal derivable_def: LEMMA derivable(f, x) IFF (EXISTS (l: real): (FORALL epsilon: EXISTS delta: FORALL (h: nzreal): abs(h) < delta IMPLIES abs((f(x + h) - f(x)) / h - l) < epsilon)) deriv_def: LEMMA (derivable(f, x) AND deriv(f,x) = L) IFF (FORALL epsilon: EXISTS delta: FORALL (h: nzreal): abs(h) < delta IMPLIES abs((f(x + h) - f(x)) / h - L) < epsilon) ff: VAR deriv_fun deriv_fun_def: LEMMA deriv(ff)(x) = L IFF (FORALL epsilon: EXISTS delta: FORALL (h: nzreal): abs(h) < delta IMPLIES abs((ff(x + h) - ff(x)) / h - L) < epsilon) END derivative_def