proposition: Lemma is_lim_spec : forall f x l, is_lim' f x l <-> is_lim f x l.
proof: Proof. destruct l as [l| |] ; split. - intros H P [eps LP]. unfold filtermap. generalize (H eps). apply filter_imp. intros u. apply LP. - intros H eps. apply (H (fun y => Rabs (y - l) < eps)). now exists eps. - intros H P [M LP]. unfold filtermap. generalize (H M). apply filter_imp. intros u. apply LP. - intros H M. apply (H (fun y => M < y)). now exists M. - intros H P [M LP]. unfold filtermap. generalize (H M). apply filter_imp. intros u. apply LP. - intros H M. apply (H (fun y => y < M)). now exists M. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq