author paulson Sat, 29 May 2021 13:42:26 +0100 changeset 73792 a1086aebcd78 parent 73789 aab7975fa070 (current diff) parent 73791 e10d530f157a (diff) child 73793 26c0ccf17f31
merged
```--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri May 28 20:21:25 2021 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sat May 29 13:42:26 2021 +0100
@@ -763,6 +763,18 @@
using bounded_minus_comp [of fst "S \<times> T" snd] assms
by (auto simp: split_def split: if_split_asm)

+lemma bounded_sums:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "bounded S" and "bounded T"
+  shows "bounded (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+  using assms by (simp add: bounded_iff) (meson norm_triangle_mono)
+
+lemma bounded_differences:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "bounded S" and "bounded T"
+  shows "bounded (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})"
+
lemma not_bounded_UNIV[simp]:
"\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
proof (auto simp: bounded_pos not_le)
@@ -1292,6 +1304,28 @@
using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
qed

+lemma compact_sums':
+  fixes S :: "'a::real_normed_vector set"
+  assumes "compact S" and "compact T"
+  shows "compact (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
+proof -
+  have "(\<Union>x\<in>S. \<Union>y\<in>T. {x + y}) = {x + y |x y. x \<in> S \<and> y \<in> T}"
+    by blast
+  then show ?thesis
+    using compact_sums [OF assms] by simp
+qed
+
+lemma compact_differences':
+  fixes S :: "'a::real_normed_vector set"
+  assumes "compact S" and "compact T"
+  shows "compact (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})"
+proof -
+  have "(\<Union>x\<in>S. \<Union>y\<in>T. {x - y}) = {x - y |x y. x \<in> S \<and> y \<in> T}"
+    by blast
+  then show ?thesis
+    using compact_differences [OF assms] by simp
+qed
+
lemma compact_translation:
"compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set"
proof -```
```--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri May 28 20:21:25 2021 +0000
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Sat May 29 13:42:26 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>```