proposition: Lemma continuity_2d_pt_filterlim : forall f x y, continuity_2d_pt f x y <-> filterlim (fun z : R * R => f (fst z) (snd z)) (locally (x,y)) (locally (f x y)).
proof: Proof. split. - intros Cf P [eps He]. specialize (Cf eps). apply locally_2d_locally in Cf. apply filter_imp with (2 := Cf). intros [u v]. apply He. - intros Cf eps. apply locally_2d_locally. specialize (Cf (fun z => Rabs (z - f x y) < eps)). unfold filtermap in Cf. apply Cf. now exists eps. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq