nicer statement of Liouville_theorem
authorpaulson <lp15@cam.ac.uk>
Fri, 28 May 2021 14:43:06 +0100
changeset 74044 370ce138d1bd
parent 74043 493b1ae188da
child 74045 e10d530f157a
nicer statement of Liouville_theorem
src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Wed May 26 18:07:49 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri May 28 14:43:06 2021 +0100
@@ -2482,12 +2482,13 @@
 theorem Liouville_theorem:
     assumes holf: "f holomorphic_on UNIV"
         and bf: "bounded (range f)"
-    obtains c where "\<And>z. f z = c"
+      shows "f constant_on UNIV"
 proof -
   obtain B where "\<And>z. cmod (f z) \<le> B"
     by (meson bf bounded_pos rangeI)
   then show ?thesis
-    using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
+    using Liouville_polynomial [OF holf, of 0 B 0, simplified]
+    by (meson constant_on_def)
 qed
 
 text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>