merged
authorwenzelm
Mon, 31 Mar 2014 21:15:26 +0200
changeset 56343 97d6a786e0f9
parent 56332 289dd9166d04 (diff)
parent 56342 075397022503 (current diff)
child 56344 1014f44c62a2
merged
--- a/src/HOL/Complex.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Complex.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -232,6 +232,8 @@
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
+declare [[coercion complex_of_real]]
+
 lemma complex_of_real_def: "complex_of_real r = Complex r 0"
   by (simp add: of_real_def complex_scaleR_def)
 
--- a/src/HOL/Limits.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Limits.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -1164,6 +1164,25 @@
   using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
   unfolding filterlim_uminus_at_bot by simp
 
+lemma filterlim_pow_at_top:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "0 < n" and f: "LIM x F. f x :> at_top"
+  shows "LIM x F. (f x)^n :: real :> at_top"
+using `0 < n` proof (induct n)
+  case (Suc n) with f show ?case
+    by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top)
+qed simp
+
+lemma filterlim_pow_at_bot_even:
+  fixes f :: "real \<Rightarrow> real"
+  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top"
+  using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_top)
+
+lemma filterlim_pow_at_bot_odd:
+  fixes f :: "real \<Rightarrow> real"
+  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
+  using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
+
 lemma filterlim_tendsto_add_at_top: 
   assumes f: "(f ---> c) F"
   assumes g: "LIM x F. g x :> at_top"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -6,7 +6,6 @@
 
 theory Complex_Analysis_Basics
 imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
-
 begin
 
 subsection {*Complex number lemmas *}
@@ -28,11 +27,11 @@
     done
 qed
 
-lemma continuous_Re: "continuous_on UNIV Re"
+lemma continuous_Re: "continuous_on X Re"
   by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
             continuous_on_cong continuous_on_id)
 
-lemma continuous_Im: "continuous_on UNIV Im"
+lemma continuous_Im: "continuous_on X Im"
   by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
             continuous_on_cong continuous_on_id)
 
@@ -52,95 +51,29 @@
   apply (simp add: algebra_simps of_nat_mult)
   done
 
-lemma open_halfspace_Re_lt: "open {z. Re(z) < b}"
-proof -
-  have "{z. Re(z) < b} = Re -`{..<b}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Re_gt: "open {z. Re(z) > b}"
-proof -
-  have "{z. Re(z) > b} = Re -`{b<..}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
-proof -
-  have "{z. Re(z) \<ge> b} = - {z. Re(z) < b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Re_lt)
-qed
-
-lemma closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
-proof -
-  have "{z. Re(z) \<le> b} = - {z. Re(z) > b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Re_gt)
-qed
-
-lemma closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
-proof -
-  have "{z. Re(z) = b} = {z. Re(z) \<le> b} \<inter> {z. Re(z) \<ge> b}"
-    by auto
-  then show ?thesis
-    by (auto simp: closed_Int closed_halfspace_Re_le closed_halfspace_Re_ge)
-qed
-
-lemma open_halfspace_Im_lt: "open {z. Im(z) < b}"
-proof -
-  have "{z. Im(z) < b} = Im -`{..<b}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Im_gt: "open {z. Im(z) > b}"
-proof -
-  have "{z. Im(z) > b} = Im -`{b<..}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
-proof -
-  have "{z. Im(z) \<ge> b} = - {z. Im(z) < b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Im_lt)
-qed
-
-lemma closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
-proof -
-  have "{z. Im(z) \<le> b} = - {z. Im(z) > b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Im_gt)
-qed
-
-lemma closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
-proof -
-  have "{z. Im(z) = b} = {z. Im(z) \<le> b} \<inter> {z. Im(z) \<ge> b}"
-    by auto
-  then show ?thesis
-    by (auto simp: closed_Int closed_halfspace_Im_le closed_halfspace_Im_ge)
-qed
+lemma
+  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
+    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
+    and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
+    and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
+    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
+    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
+    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
+    and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
+    and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
+    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
+  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
+            isCont_Im isCont_ident isCont_const)+
 
 lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
 
 lemma closed_complex_Reals: "closed (Reals :: complex set)"
 proof -
-  have "-(Reals :: complex set) = {z. Im(z) < 0} \<union> {z. 0 < Im(z)}"
+  have "(Reals :: complex set) = {z. Im z = 0}"
     by (auto simp: complex_is_Real_iff)
   then show ?thesis
-    by (metis closed_def open_Un open_halfspace_Im_gt open_halfspace_Im_lt)
+    by (metis closed_halfspace_Im_eq)
 qed
 
 
@@ -218,25 +151,8 @@
 
 lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  assumes "uniformly_continuous_on s f"
-  shows "uniformly_continuous_on s (\<lambda>x. f x * c)"
-proof (cases "c=0")
-  case True then show ?thesis
-    by (simp add: uniformly_continuous_on_const)
-next
-  case False show ?thesis
-    apply (rule bounded_linear.uniformly_continuous_on)
-    apply (metis bounded_linear_ident)
-    using assms
-    apply (auto simp: uniformly_continuous_on_def dist_norm)
-    apply (drule_tac x = "e / norm c" in spec, auto)
-    apply (metis divide_pos_pos zero_less_norm_iff False)
-    apply (rule_tac x=d in exI, auto)
-    apply (drule_tac x = x in bspec, assumption)
-    apply (drule_tac x = "x'" in bspec)
-    apply (auto simp: False less_divide_eq)
-    by (metis dual_order.strict_trans2 left_diff_distrib norm_mult_ineq)
-qed
+  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
+  by (metis bounded_linear.uniformly_continuous_on[of "\<lambda>x. x * c"] bounded_linear_mult_left) 
 
 lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
@@ -259,62 +175,6 @@
 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
   by auto
 
-lemma has_derivative_zero_constant:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "convex s"
-      and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    shows "\<exists>c. \<forall>x\<in>s. f x = c"
-proof (cases "s={}")
-  case False
-  then obtain x where "x \<in> s"
-    by auto
-  have d0': "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    by (metis d0)
-  have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
-  proof -
-    case goal1
-    then show ?case
-      using differentiable_bound[OF assms(1) d0', of 0 x y] and `x \<in> s`
-      unfolding onorm_zero
-      by auto
-  qed
-  then show ?thesis 
-    by metis
-next
-  case True
-  then show ?thesis by auto
-qed
-
-lemma has_derivative_zero_unique:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "convex s"
-      and "\<And>x. x\<in>s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
-      and "a \<in> s"
-      and "x \<in> s"
-    shows "f x = f a"
-  using assms
-  by (metis has_derivative_zero_constant)
-
-lemma has_derivative_zero_connected_constant:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
-  assumes "connected s"
-      and "open s"
-      and "finite k"
-      and "continuous_on s f"
-      and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
-proof (cases "s = {}")
-  case True
-  then show ?thesis
-by (metis empty_iff that)
-next
-  case False
-  then obtain c where "c \<in> s"
-    by (metis equals0I)
-  then show ?thesis
-    by (metis has_derivative_zero_unique_strong_connected assms that)
-qed
-
 lemma DERIV_zero_connected_constant:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   assumes "connected s"
@@ -342,8 +202,8 @@
       and "a \<in> s"
       and "x \<in> s"
     shows "f x = f a"
-apply (rule has_derivative_zero_unique [where f=f, OF assms(1) _ assms(3,4)])
-by (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
+  by (rule has_derivative_zero_unique [where f=f, OF assms(1,3) refl _ assms(4)])
+     (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
 
 lemma DERIV_zero_connected_unique:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
@@ -353,7 +213,7 @@
       and "a \<in> s"
       and "x \<in> s"
     shows "f x = f a" 
-    apply (rule Integration.has_derivative_zero_unique_strong_connected [of s "{}" f])
+    apply (rule has_derivative_zero_unique_strong_connected [of s "{}" f])
     using assms
     apply auto
     apply (metis DERIV_continuous_on)
@@ -365,7 +225,7 @@
       and "\<And>x. x\<in>s \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
     shows "(g has_field_derivative f') (at a within s)"
   using assms unfolding has_field_derivative_def
-  by (blast intro: Derivative.has_derivative_transform_within)
+  by (blast intro: has_derivative_transform_within)
 
 lemma DERIV_transform_within_open:
   assumes "DERIV f a :> f'"
@@ -1177,21 +1037,18 @@
 lemma continuous_on_cnj: "continuous_on s cnj"
 by (metis bounded_linear_cnj linear_continuous_on)
 
-subsection{*Some limit theorems about real part of real series etc.*}
+subsection {*Some limit theorems about real part of real series etc.*}
 
 lemma real_lim:
   fixes l::complex
-  assumes "(f ---> l) F" and " ~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
+  assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   shows  "l \<in> \<real>"
-proof -
-  have 1: "((\<lambda>i. Im (f i)) ---> Im l) F"
-    by (metis assms(1) tendsto_Im) 
-  then have  "((\<lambda>i. Im (f i)) ---> 0) F" using assms
-    by (metis (mono_tags, lifting) Lim_eventually complex_is_Real_iff eventually_mono)
-  then show ?thesis using 1
-    by (metis 1 assms(2) complex_is_Real_iff tendsto_unique) 
-qed
-
+proof (rule Lim_in_closed_set)
+  show "closed (\<real>::complex set)"
+    by (rule closed_complex_Reals)
+  show "eventually (\<lambda>x. f x \<in> \<real>) F"
+    using assms(3, 4) by (auto intro: eventually_mono)
+qed fact+
 lemma real_lim_sequentially:
   fixes l::complex
   shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
@@ -1209,14 +1066,6 @@
   by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
 
 
-lemma norm_setsum_bound:
-  fixes n::nat
-  shows" \<lbrakk>\<And>n. N \<le> n \<Longrightarrow> norm (f n) \<le> g n; N \<le> m\<rbrakk>
-       \<Longrightarrow> norm (setsum f {m..<n}) \<le> setsum g {m..<n}"
-apply (induct n, auto)
-by (metis dual_order.trans le_cases le_neq_implies_less norm_triangle_mono)
-
-
 (*MOVE? But not to Finite_Cartesian_Product*)
 lemma sums_vec_nth :
   assumes "f sums a"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -883,25 +883,14 @@
   assumes "convex s"
     and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
   shows "\<exists>c. \<forall>x\<in>s. f x = c"
-proof (cases "s={}")
-  case False
-  then obtain x where "x \<in> s"
-    by auto
-  have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
-  proof -
-    case goal1
-    then show ?case
-      using differentiable_bound[OF assms(1-2), of 0 x y] and `x \<in> s`
-      unfolding onorm_zero
-      by auto
-  qed
+proof -
+  { fix x y assume "x \<in> s" "y \<in> s"
+    then have "norm (f x - f y) \<le> 0 * norm (x - y)"
+      using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
+    then have "f x = f y"
+      by simp }
   then show ?thesis
-    apply (rule_tac x="f x" in exI)
-    apply auto
-    done
-next
-  case True
-  then show ?thesis by auto
+    by metis
 qed
 
 lemma has_derivative_zero_unique:
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -8869,6 +8869,26 @@
     using `x \<in> s` `f c = y` `c \<in> s` by auto
 qed
 
+lemma has_derivative_zero_connected_constant:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+  assumes "connected s"
+      and "open s"
+      and "finite k"
+      and "continuous_on s f"
+      and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
+proof (cases "s = {}")
+  case True
+  then show ?thesis
+by (metis empty_iff that)
+next
+  case False
+  then obtain c where "c \<in> s"
+    by (metis equals0I)
+  then show ?thesis
+    by (metis has_derivative_zero_unique_strong_connected assms that)
+qed
+
 
 subsection {* Integrating characteristic function of an interval *}
 
--- a/src/HOL/Set_Interval.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -414,6 +414,11 @@
   using dense[of "a" "min c b"] dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
 
+lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff:
+  "{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "a" "min c b"] dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
 end
 
 context no_top
@@ -463,6 +468,88 @@
 by (auto simp: set_eq_iff intro: top_le le_bot)
 
 
+subsection {* Infinite intervals *}
+
+context dense_linorder
+begin
+
+lemma infinite_Ioo:
+  assumes "a < b"
+  shows "\<not> finite {a<..<b}"
+proof
+  assume fin: "finite {a<..<b}"
+  moreover have ne: "{a<..<b} \<noteq> {}"
+    using `a < b` by auto
+  ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b"
+    using Max_in[of "{a <..< b}"] by auto
+  then obtain x where "Max {a <..< b} < x" "x < b"
+    using dense[of "Max {a<..<b}" b] by auto
+  then have "x \<in> {a <..< b}"
+    using `a < Max {a <..< b}` by auto
+  then have "x \<le> Max {a <..< b}"
+    using fin by auto
+  with `Max {a <..< b} < x` show False by auto
+qed
+
+lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}"
+  using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b]
+  by (auto dest: finite_subset)
+
+lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}"
+  using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b]
+  by (auto dest: finite_subset)
+
+lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}"
+  using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b]
+  by (auto dest: finite_subset)
+
+end
+
+lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}"
+proof
+  assume "finite {..< a}"
+  then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x"
+    by auto
+  obtain x where "x < a"
+    using lt_ex by auto
+
+  obtain y where "y < Min {..< a}"
+    using lt_ex by auto
+  also have "Min {..< a} \<le> x"
+    using `x < a` by fact
+  also note `x < a`
+  finally have "Min {..< a} \<le> y"
+    by fact
+  with `y < Min {..< a}` show False by auto
+qed
+
+lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}"
+  using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"]
+  by (auto simp: subset_eq less_imp_le)
+
+lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}"
+proof
+  assume "finite {a <..}"
+  then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}"
+    by auto
+
+  obtain y where "Max {a <..} < y"
+    using gt_ex by auto
+
+  obtain x where "a < x"
+    using gt_ex by auto
+  also then have "x \<le> Max {a <..}"
+    by fact
+  also note `Max {a <..} < y`
+  finally have "y \<le> Max { a <..}"
+    by fact
+  with `Max {a <..} < y` show False by auto
+qed
+
+lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}"
+  using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"]
+  by (auto simp: subset_eq less_imp_le)
+
 subsubsection {* Intersection *}
 
 context linorder
@@ -823,6 +910,7 @@
      "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
 
+
 text{* Any subset of an interval of natural numbers the size of the
 subset is exactly that interval. *}
 
--- a/src/HOL/Topological_Spaces.thy	Mon Mar 31 21:13:51 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Mar 31 21:15:26 2014 +0200
@@ -2134,8 +2134,37 @@
 lemma connected_empty[simp]: "connected {}"
   by (auto intro!: connectedI)
 
+lemma connectedD:
+  "connected A \<Longrightarrow> open U \<Longrightarrow> open V \<Longrightarrow> U \<inter> V \<inter> A = {} \<Longrightarrow> A \<subseteq> U \<union> V \<Longrightarrow> U \<inter> A = {} \<or> V \<inter> A = {}" 
+  by (auto simp: connected_def)
+
 end
 
+lemma connected_local_const:
+  assumes "connected A" "a \<in> A" "b \<in> A"
+  assumes *: "\<forall>a\<in>A. eventually (\<lambda>b. f a = f b) (at a within A)"
+  shows "f a = f b"
+proof -
+  obtain S where S: "\<And>a. a \<in> A \<Longrightarrow> a \<in> S a" "\<And>a. a \<in> A \<Longrightarrow> open (S a)"
+    "\<And>a x. a \<in> A \<Longrightarrow> x \<in> S a \<Longrightarrow> x \<in> A \<Longrightarrow> f a = f x"
+    using * unfolding eventually_at_topological by metis
+
+  let ?P = "\<Union>b\<in>{b\<in>A. f a = f b}. S b" and ?N = "\<Union>b\<in>{b\<in>A. f a \<noteq> f b}. S b"
+  have "?P \<inter> A = {} \<or> ?N \<inter> A = {}"
+    using `connected A` S `a\<in>A`
+    by (intro connectedD) (auto, metis)
+  then show "f a = f b"
+  proof
+    assume "?N \<inter> A = {}"
+    then have "\<forall>x\<in>A. f a = f x"
+      using S(1) by auto
+    with `b\<in>A` show ?thesis by auto
+  next
+    assume "?P \<inter> A = {}" then show ?thesis
+      using `a \<in> A` S(1)[of a] by auto
+  qed
+qed
+
 lemma (in linorder_topology) connectedD_interval:
   assumes "connected U" and xy: "x \<in> U" "y \<in> U" and "x \<le> z" "z \<le> y"
   shows "z \<in> U"