summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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})" + using assms by (simp add: bounded_iff) (meson add_mono norm_triangle_le_diff) + 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>