proposition: Lemma circle_cover_continuous : continuous circle_cover.
proof: Proof. apply product2_map_continuous. - apply (@continuous_composition RTop RTop RTop cos). { apply cos_continuous. } apply (@continuous_composition_2arg RTop RTop RTop). + apply continuous_constant. + apply continuous_identity. + apply Rmult_continuous. - apply (@continuous_composition RTop RTop RTop sin). { apply sin_continuous. } apply (@continuous_composition_2arg RTop RTop RTop). + apply continuous_constant. + apply continuous_identity. + apply Rmult_continuous. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)