proposition: Lemma connected_img: forall {X Y:TopologicalSpace} (f:point_set X -> point_set Y), connected X -> continuous f -> surjective f -> connected Y.
proof: Proof. intros. red. intros. destruct (H (inverse_image f S)). - apply continuous_clopen; assumption. - left. extensionality_ensembles. destruct (H1 x). eapply False_ind, Noone_in_empty. rewrite <- H3. constructor. now rewrite H5. - right. extensionality_ensembles. + constructor. + destruct (H1 x). rewrite <- H4. apply in_inverse_image. now rewrite H3. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)