derivative_def_ax: THEORY BEGIN f: VAR [real -> real] x,L: VAR real IMPORTING derivatives_ax epsilon, delta: VAR posreal derivative_def: AXIOM 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: AXIOM (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[real] deriv_fun_def: AXIOM 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_ax