--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Mon Sep 25 17:06:11 2023 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Wed Sep 27 13:34:15 2023 +0100
@@ -1121,6 +1121,11 @@
by (metis Diff_empty contour_integrable_holomorphic finite.emptyI g os)
qed
+lemma analytic_imp_contour_integrable:
+ assumes "f analytic_on path_image p" "valid_path p"
+ shows "f contour_integrable_on p"
+ by (meson analytic_on_holomorphic assms contour_integrable_holomorphic_simple)
+
lemma continuous_on_inversediff:
fixes z:: "'a::real_normed_field" shows "z \<notin> S \<Longrightarrow> continuous_on S (\<lambda>w. 1 / (w - z))"
by (rule continuous_intros | force)+