src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 66827 c94531b5007d
parent 66486 ffaaa83543b2
child 67135 1a94352812f4
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 10 14:03:51 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 10 17:15:37 2017 +0100
     1.3 @@ -497,7 +497,7 @@
     1.4  lemma analytic_on_imp_differentiable_at:
     1.5    "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f field_differentiable (at x)"
     1.6   apply (auto simp: analytic_on_def holomorphic_on_def)
     1.7 -by (metis Topology_Euclidean_Space.open_ball centre_in_ball field_differentiable_within_open)
     1.8 +by (metis open_ball centre_in_ball field_differentiable_within_open)
     1.9  
    1.10  lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
    1.11    by (auto simp: analytic_on_def)
    1.12 @@ -521,7 +521,7 @@
    1.13      then show "\<exists>t. open t \<and> s \<subseteq> t \<and> f analytic_on t"
    1.14        apply (simp add: analytic_on_def)
    1.15        apply (rule exI [where x="\<Union>{u. open u \<and> f analytic_on u}"], auto)
    1.16 -      apply (metis Topology_Euclidean_Space.open_ball analytic_on_open centre_in_ball)
    1.17 +      apply (metis open_ball analytic_on_open centre_in_ball)
    1.18        by (metis analytic_on_def)
    1.19    next
    1.20      fix t
    1.21 @@ -652,7 +652,7 @@
    1.22    have "continuous_on (ball z e) f"
    1.23      by (metis fh holomorphic_on_imp_continuous_on)
    1.24    then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
    1.25 -    by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz)
    1.26 +    by (metis open_ball centre_in_ball continuous_on_open_avoid e z nz)
    1.27    have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
    1.28      apply (rule holomorphic_on_inverse)
    1.29      apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball)