proposition: Lemma quotient_connected {X : TopologicalSpace} (R : Relation X) : connected X -> connected (QuotientTopology R).
proof: Proof. intros H U [H1 H2]. destruct (H (inverse_image (quotient_projection R) U)). - split; [ | red; rewrite <- inverse_image_complement ]; now apply quotient_projection_continuous. - left. eapply inverse_image_surjective_injective. + apply quotient_projection_surjective'. + now rewrite inverse_image_empty. - right. eapply inverse_image_surjective_injective. + apply quotient_projection_surjective'. + now rewrite inverse_image_full. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)