src/HOL/Analysis/Complex_Transcendental.thy
changeset 64508 874555896035
parent 64394 141e1ed8d5a0
child 64593 50c715579715
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Nov 19 19:43:09 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Nov 19 20:10:32 2016 +0100
     1.3 @@ -3265,8 +3265,8 @@
     1.4  
     1.5  lemma homotopic_circlemaps_imp_homotopic_loops:
     1.6    assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
     1.7 -   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
     1.8 -                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
     1.9 +   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
    1.10 +                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
    1.11  proof -
    1.12    have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
    1.13      using assms by (auto simp: sphere_def)
    1.14 @@ -3347,7 +3347,7 @@
    1.15        and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
    1.16      shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
    1.17  proof -
    1.18 -  have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * ii))"
    1.19 +  have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * \<i>))"
    1.20      apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
    1.21      apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
    1.22      done