proposition: Lemma quotient_projection_open_iff {X : TopologicalSpace} (R : Relation X) (U : Ensemble (QuotientTopology R)) : open (inverse_image (quotient_projection R) U) <-> open U.
proof: Proof. split. - now intros H []. - apply quotient_projection_continuous. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)