fact: Definition Vderivable_pt_lim (f : R -> V) (I : R -> Prop) (x : R) (l : V) := I x -> forall eps : R, 0 < eps -> {delta : R | delta > 0 /\ (forall h : R, h <> 0 -> Rabs h < delta -> I (x + h) -> (N (vsub (smul (/h) (vsub (f (x + h)) (f x) )) l )) < eps)}.
imports: Reals integrales