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