proposition: Lemma continuous_at_neighborhood_basis: forall (x:X) (NB:Family Y), neighborhood_basis NB (f x) -> (forall V:Ensemble Y, In NB V -> neighborhood (inverse_image f V) x) -> continuous_at x.
proof: Proof. intros. red; intros. destruct H. apply neighborhood_basis_cond in H1. destruct H1 as [N [? ?]]. pose proof (H0 N H). destruct H2 as [U [? ?]]. exists U; split; trivial. assert (Included (inverse_image f N) (inverse_image f V)); auto with sets. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases