proposition: Lemma quotient_projection_continuous {X : TopologicalSpace} (R : Relation X) : @continuous X (QuotientTopology R) (quotient_projection R).
proof: Proof. intros U HU. now apply strong_topology_makes_continuous_funcs with (a:=I) in HU. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)