proposition: Lemma factorization_is_continuous: continuous continuous_factorization.
proof: Proof. red. intros. rewrite subspace_open_char in H. destruct H as [V' []]. subst V. rewrite <- inverse_image_composition. simpl. replace (inverse_image (fun x:X => f x) V') with (inverse_image f V'). - now apply f_cont. - extensionality_ensembles; now constructor. Qed.
imports: ZornsLemma(EnsemblesTactics) TopologicalSpaces Continuity SubspaceTopology