proposition: Lemma induced_function_continuous {X : TopologicalSpace} (R : relation X) (Y : TopologicalSpace) (f : X -> Y) (Hf : forall x0 x1, R x0 x1 -> f x0 = f x1) (HR : equivalence R) : continuous f -> @continuous (QuotientTopology R) Y (induced_function _ HR Hf).
proof: Proof. intros. apply StrongTopology.strong_topology_continuous_char. intros []. simpl. unfold compose. apply (continuous_funext f); auto. intros. symmetry. apply induced_function_correct. Qed.
imports: ZornsLemma(Finite_sets Quotients) Topology(Connectedness Compactness CountabilityAxioms StrongTopology)