proposition: Lemma continuous_closed : continuous <-> forall U, closed U -> closed (inverse_image f U).
proof: Proof. split. - intros. red. rewrite <- inverse_image_complement. apply H. assumption. - intros. red. intros. apply closed_complement_open. rewrite <- inverse_image_complement. apply H. red. rewrite Complement_Complement. assumption. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases NeighborhoodBases Subbases