proposition: Lemma continuous_function_preserves_filter_limits: forall (X Y:TopologicalSpace) (f:point_set X -> point_set Y) (x:point_set X) (F:Filter X), filter_limit F x -> continuous_at f x -> filter_limit (filter_direct_image f F) (f x).
proof: Proof. intros. red; intros. intros V ?. destruct H1. constructor. cut (In (filter_family (neighborhood_filter x)) (inverse_image f V)). { apply H. } constructor. apply H0; trivial. Qed.
imports: ZornsLemma(Powerset_facts)