proposition: Lemma quotient_compact {X : TopologicalSpace} (R : Relation X) : compact X -> compact (QuotientTopology R).
proof: Proof. intros H F HF eqF. apply (f_equal (inverse_image (quotient_projection R))) in eqF. rewrite inverse_image_full, inverse_image_family_union_image in eqF. apply H in eqF. - destruct eqF as [F' [H1 [H2 H3]]]. exists (inverse_image (inverse_image (quotient_projection R)) F'). repeat split. + apply injective_finite_inverse_image; auto. apply inverse_image_surjective_injective. apply quotient_projection_surjective'. + intros U [H4]. apply H2 in H4. inversion H4. subst. apply inverse_image_surjective_injective in H5. * now subst. * apply quotient_projection_surjective'. + extensionality_ensembles_inv. * constructor. * destruct (quotient_projection_surjective' _ x). assert (In (FamilyUnion F') x1) as H6 by now rewrite H3. destruct H6, (H2 _ H5). subst. destruct H6. repeat econstructor; eassumption. - intros U [? ? ? ?]. subst. now apply quotient_projection_open_iff, HF. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)