proposition: Lemma continuous_func_preserves_net_limits: forall {I:DirectedSet} (x:Net I X) (x0:X), net_limit x x0 -> continuous_at f x0 -> net_limit (fun i:DS_set I => f (x i)) (f x0).
proof: Proof. intros. red. intros V ? ?. assert (neighborhood V (f x0)). { apply open_neighborhood_is_neighborhood. now split. } destruct (H0 V H3) as [U [? ?]]. destruct H4. pose proof (H U H4 H6). apply eventually_impl_base with (fun i:DS_set I => In U (x i)); trivial. intros. assert (In (inverse_image f V) (x i)) by auto with sets. now destruct H9. Qed.