proposition: Lemma func_preserving_net_limits_is_continuous: forall x0:X, (forall (I:DirectedSet) (x:Net I X), net_limit x x0 -> net_limit (fun i:DS_set I => f (x i)) (f x0)) -> continuous_at f x0.
proof: Proof. intros. pose proof (H (neighborhood_net_DS X x0) (neighborhood_net X x0) (neighborhood_net_limit X x0)). apply continuous_at_open_neighborhoods. intros. destruct H1, (H0 V H1 H2). destruct x as [U]. exists U. repeat split; trivial. apply (H3 (intro_neighborhood_net_DS X x0 U x o i H4)). simpl. auto with sets. Qed.