equal
deleted
inserted
replaced
978 have fz0: "f z = 0" if "0 < r" and lt1: "\<And>x. x \<noteq> 0 \<Longrightarrow> cmod x < r \<Longrightarrow> inverse (cmod (f (inverse x))) < 1" |
978 have fz0: "f z = 0" if "0 < r" and lt1: "\<And>x. x \<noteq> 0 \<Longrightarrow> cmod x < r \<Longrightarrow> inverse (cmod (f (inverse x))) < 1" |
979 for z r |
979 for z r |
980 proof - |
980 proof - |
981 have f0: "(f \<longlongrightarrow> 0) at_infinity" |
981 have f0: "(f \<longlongrightarrow> 0) at_infinity" |
982 proof - |
982 proof - |
983 have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment>\<open>should not be necessary!\<close> |
983 have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment> \<open>should not be necessary!\<close> |
984 by simp |
984 by simp |
985 have "continuous_on (inverse ` (ball 0 r - {0})) f" |
985 have "continuous_on (inverse ` (ball 0 r - {0})) f" |
986 using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast |
986 using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast |
987 then have "connected ((f \<circ> inverse) ` (ball 0 r - {0}))" |
987 then have "connected ((f \<circ> inverse) ` (ball 0 r - {0}))" |
988 apply (intro connected_continuous_image continuous_intros) |
988 apply (intro connected_continuous_image continuous_intros) |