proposition: Lemma continuous_at_open_neighborhoods: forall x:X, (forall V:Ensemble Y, open_neighborhood V (f x) -> neighborhood (inverse_image f V) x) -> continuous_at x.
proof: Proof. intros. red; intros. destruct H0 as [V' [? ?]]. pose proof (H V' H0). destruct H2 as [U' [? ?]]. exists U'; split; trivial. apply (inverse_image_increasing f) in H1; auto with sets. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases