proposition: Lemma continuous_iff_continuity {f : R -> R} : @continuous RTop RTop f <-> continuity f.
proof: Proof. split; intros H ?. - now apply continuous_at_iff_continuity_pt, continuous_func_continuous_everywhere. - apply pointwise_continuity. intro. now apply continuous_at_iff_continuity_pt. Qed.
imports: RTopology ProductTopology Homeomorphisms ContinuousFactorization Coq(FunctionalExtensionality Lra ProofIrrelevance) ZornsLemma(EnsembleProduct EnsemblesTactics)