proposition: Lemma continuity_pt_filterlim' : forall f x, continuity_pt f x <-> filterlim f (locally' x) (locally (f x)).
proof: Proof. intros f x. eapply iff_trans. apply continuity_pt_locally'. apply iff_sym. exact (filterlim_locally f (f x)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub