proposition: Lemma f_inv_continuous : continuous f_inv.
proof: Proof. apply induced_function_continuous. apply subspace_continuous_char. unfold compose. simpl. apply (continuous_composition circle_cover). - apply circle_cover_continuous. - apply subspace_inc_continuous. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)