proposition: Lemma continuous_surj_factorization_is_continuous: continuous continuous_surj_factorization.
proof: Proof. now apply factorization_is_continuous. Qed.
imports: ZornsLemma(EnsemblesTactics) TopologicalSpaces Continuity SubspaceTopology