proposition: Lemma f_inv_bijective : bijective f_inv.
proof: Proof. split. - intros [x Hx] [y Hy]. intros. apply subset_eq; simpl. inversion Hx as [x0 _]; subst. inversion Hy as [y0 _]; subst. apply R_impl_equality_of_equiv_class. { apply SpaceAdjunction_equivalence. } unfold f_inv in H. rewrite !induced_function_correct in H. clear Hx Hy. destruct x0 as [x Hx0]. destruct y0 as [y Hy0]. simpl in *. assert (circle_cover x = circle_cover y). { inversion H; subst. unfold circle_cover. congruence. } clear H. destruct Hx0 as [Hx0], Hy0 as [Hy0]. apply circle_cover_preimage in H0 as [z Hz]. assert (-1 <= z <= 1)%Z. { split; apply le_IZR; lra. } destruct z. + assert (x = y) by lra. subst. left. apply subset_eq. reflexivity. + destruct p; try lia. assert (x = 1) by lra. assert (y = 0) by lra. subst. replace (exist _ 1 _) with U1. 2: { apply subset_eq. reflexivity. } replace (exist _ 0 _) with U0. 2: { apply subset_eq. reflexivity. } right. split; [right|left]. + destruct p; try lia. assert (x = 0) by lra. assert (y = 1) by lra. subst. replace (exist _ 1 _) with U1. 2: { apply subset_eq. reflexivity. } replace (exist _ 0 _) with U0. 2: { apply subset_eq. reflexivity. } right. split; [left|right]. - red. intros y. exists (f y). unfold f_inv, f. simpl. unfold quotient_projection. rewrite (induced_function_correct (fun x : { x : RTop | _} => exist (In S1_Ensemble) (circle_cover (subspace_inc _ x)) _)). apply subset_eq. simpl. unfold f1. destruct y as [[x y] H]. simpl. replace (circle_cover _) with (if Rle_lt_dec y 0 then circle_cover (1 - acos x / (2*PI)) else circle_cover (acos x / (2 * PI))). 2: { destruct (Rle_lt_dec y 0); auto. } unfold circle_cover. rewrite !Rmult_minus_distr_l. rewrite Rmult_1_r. rewrite cos_2PI_neg. rewrite sin_2PI_neg. destruct H. pose proof (Rsqr_sum_1_bound_l _ _ H). replace (_ * _ * (acos x / _)) with (acos x). 2: { pose proof PI_neq0. unfold Rdiv. rewrite Rmult_comm. rewrite Rmult_assoc. replace (/ _ * _) with 1; try lra. symmetry. apply Rinv_l. lra. } rewrite cos_acos; auto. replace (sin (acos x)) with (sqrt y²). 2: { rewrite sin_acos; auto. apply f_equal. lra. } rewrite sqrt_Rsqr_abs. unfold Rabs. destruct (Rle_lt_dec y 0), (Rcase_abs y); auto; try lra. + rewrite Ropp_involutive. reflexivity. + assert (y = 0) by lra. subst. rewrite Ropp_0. reflexivity. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)