more symbols;
authorwenzelm
Sat Nov 19 20:10:32 2016 +0100 (2016-11-19)
changeset 64508874555896035
parent 64507 eace715f4988
child 64509 80aaa4ff7fed
more symbols;
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Further_Topology.thy
     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
     2.1 --- a/src/HOL/Analysis/Further_Topology.thy	Sat Nov 19 19:43:09 2016 +0100
     2.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Sat Nov 19 20:10:32 2016 +0100
     2.3 @@ -3240,7 +3240,7 @@
     2.4      have inj_exp: "inj_on exp (ball (Ln z) 1)"
     2.5        apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
     2.6        using pi_ge_two by (simp add: ball_subset_ball_iff)
     2.7 -    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
     2.8 +    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1))"
     2.9      show ?thesis
    2.10      proof (intro exI conjI)
    2.11        show "z \<in> exp ` (ball(Ln z) 1)"
    2.12 @@ -3286,7 +3286,7 @@
    2.13        proof
    2.14          fix u
    2.15          assume "u \<in> \<V>"
    2.16 -        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
    2.17 +        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1)"
    2.18            by (auto simp: \<V>_def)
    2.19          have "compact (cball (Ln z) 1)"
    2.20            by simp
    2.21 @@ -3325,7 +3325,7 @@
    2.22            apply (force simp:)
    2.23            done
    2.24          show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
    2.25 -          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
    2.26 +          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * \<i>) \<circ> \<gamma>" in exI)
    2.27            unfolding homeomorphism_def
    2.28            apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
    2.29               apply (auto simp: \<gamma>exp exp2n cont n)