proposition: Lemma continuous_composition: forall {X Y Z:TopologicalSpace} (f:Y -> Z) (g:X -> Y), continuous f -> continuous g -> continuous (fun x:X => f (g x)).
proof: Proof. intros. red; intros. rewrite inverse_image_composition. auto. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases