proposition: Lemma quotient_separable {X : TopologicalSpace} (R : Relation X) : separable X -> separable (QuotientTopology R).
proof: Proof. intros [S [HC HD]]. exists (Im S (quotient_projection R)). split. - unshelve refine (surj_countable (fun x => exist _ (quotient_projection R (proj1_sig x)) _) HC _). + destruct x. now econstructor; trivial. + intros [? [x H ? ?]]. exists (exist _ x H). subst. reflexivity. - now apply (dense_image_surjective S (quotient_projection_continuous R) (quotient_projection_surjective' R)). Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)