proposition: Lemma continuous_subbasis: forall (SB:Family Y), subbasis SB -> (forall V:Ensemble Y, In SB V -> open (inverse_image f V)) -> continuous.
proof: Proof. intros. apply (continuous_open_basis _ (finite_intersections_of_subbasis_form_open_basis _ _ H)). intros. induction H1. - rewrite inverse_image_full. apply open_full. - apply H0. assumption. - rewrite inverse_image_intersection. apply open_intersection2; assumption. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases