equal
deleted
inserted
replaced
3386 have "t = {} \<or> u = {}" |
3386 have "t = {} \<or> u = {}" |
3387 using assms [OF conif fi] tus [symmetric] |
3387 using assms [OF conif fi] tus [symmetric] |
3388 by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue) |
3388 by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue) |
3389 } |
3389 } |
3390 then show ?thesis |
3390 then show ?thesis |
3391 by (simp add: connected_closed_in_eq) |
3391 by (simp add: connected_closedin_eq) |
3392 qed |
3392 qed |
3393 |
3393 |
3394 lemma continuous_disconnected_range_constant_eq: |
3394 lemma continuous_disconnected_range_constant_eq: |
3395 "(connected s \<longleftrightarrow> |
3395 "(connected s \<longleftrightarrow> |
3396 (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
3396 (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1. |
6812 apply (simp add: open_contains_ball Ball_def) |
6812 apply (simp add: open_contains_ball Ball_def) |
6813 apply (erule all_forward) |
6813 apply (erule all_forward) |
6814 using "*" by auto blast+ |
6814 using "*" by auto blast+ |
6815 have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})" |
6815 have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})" |
6816 using assms |
6816 using assms |
6817 by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv) |
6817 by (auto intro: continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv) |
6818 obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] . |
6818 obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] . |
6819 then have holfb: "f holomorphic_on ball w e" |
6819 then have holfb: "f holomorphic_on ball w e" |
6820 using holf holomorphic_on_subset by blast |
6820 using holf holomorphic_on_subset by blast |
6821 have 3: "(\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}) = s \<Longrightarrow> f w = 0" |
6821 have 3: "(\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}) = s \<Longrightarrow> f w = 0" |
6822 using \<open>e>0\<close> e by (force intro: holomorphic_fun_eq_0_on_ball [OF holfb]) |
6822 using \<open>e>0\<close> e by (force intro: holomorphic_fun_eq_0_on_ball [OF holfb]) |