prove Liminf_inverse_ereal
authorhoelzl
Fri Sep 25 16:54:31 2015 +0200 (2015-09-25)
changeset 61245b77bf45efe21
parent 61244 6026c14f5e5d
child 61270 28eb608b9b59
prove Liminf_inverse_ereal
src/HOL/Filter.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Thu Sep 24 15:21:12 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Fri Sep 25 16:54:31 2015 +0200
     1.3 @@ -390,6 +390,9 @@
     1.4  lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
     1.5    by (simp add: frequently_const_iff)
     1.6  
     1.7 +lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
     1.8 +  by (metis frequentlyE eventually_frequently)
     1.9 +
    1.10  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
    1.11    where "trivial_limit F \<equiv> F = bot"
    1.12  
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Sep 24 15:21:12 2015 +0200
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 25 16:54:31 2015 +0200
     2.3 @@ -1732,6 +1732,14 @@
     2.4    apply (auto split: ereal.split simp: ereal_uminus_reorder) []
     2.5    done
     2.6  
     2.7 +lemma at_infty_ereal_eq_at_top: "at \<infinity> = filtermap ereal at_top"
     2.8 +  unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
     2.9 +    top_ereal_def[symmetric]
    2.10 +  apply (subst eventually_nhds_top[of 0])
    2.11 +  apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
    2.12 +  apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans)
    2.13 +  done
    2.14 +
    2.15  lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
    2.16    using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
    2.17    by auto
    2.18 @@ -3589,6 +3597,34 @@
    2.19    unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
    2.20    using lim_ereal by (simp_all add: comp_def)
    2.21  
    2.22 +lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
    2.23 +proof -
    2.24 +  have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
    2.25 +    by (intro tendsto_intros tendsto_inverse_0)
    2.26 +  
    2.27 +  show ?thesis
    2.28 +    by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
    2.29 +       (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
    2.30 +             intro!: filterlim_mono_eventually[OF **])
    2.31 +qed
    2.32 +
    2.33 +lemma inverse_ereal_tendsto_pos: 
    2.34 +  fixes x :: ereal assumes "0 < x"
    2.35 +  shows "inverse -- x --> inverse x"
    2.36 +proof (cases x)
    2.37 +  case (real r)
    2.38 +  with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
    2.39 +    by (auto intro!: tendsto_inverse)
    2.40 +  from real \<open>0 < x\<close> show ?thesis
    2.41 +    by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
    2.42 +             intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
    2.43 +qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
    2.44 +
    2.45 +lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \<infinity>) (at_right (0::ereal))"
    2.46 +  unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def
    2.47 +  by (subst filterlim_cong[OF refl refl, where g="\<lambda>x. ereal (inverse x)"])
    2.48 +     (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right)
    2.49 +
    2.50  lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
    2.51  
    2.52  lemma continuous_at_iff_ereal:
     3.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Sep 24 15:21:12 2015 +0200
     3.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Fri Sep 25 16:54:31 2015 +0200
     3.3 @@ -150,6 +150,17 @@
     3.4    shows "Limsup F X \<le> C"
     3.5    using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
     3.6  
     3.7 +lemma le_Limsup:
     3.8 +  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
     3.9 +  shows "l \<le> Limsup F f"
    3.10 +proof -
    3.11 +  have "l = Limsup F (\<lambda>x. l)"
    3.12 +    using F by (simp add: Limsup_const)
    3.13 +  also have "\<dots> \<le> Limsup F f"
    3.14 +    by (intro Limsup_mono x) 
    3.15 +  finally show ?thesis .
    3.16 +qed
    3.17 +
    3.18  lemma le_Liminf_iff:
    3.19    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
    3.20    shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
    3.21 @@ -308,4 +319,33 @@
    3.22    then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
    3.23  qed
    3.24  
    3.25 +lemma continuous_on_imp_continuous_within: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
    3.26 +  unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset)
    3.27 +
    3.28 +lemma Liminf_compose_continuous_antimono:
    3.29 +  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
    3.30 +  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
    3.31 +  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
    3.32 +proof -
    3.33 +  { fix P assume "eventually P F"
    3.34 +    have "\<exists>x. P x"
    3.35 +    proof (rule ccontr)
    3.36 +      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
    3.37 +        by auto
    3.38 +      with \<open>eventually P F\<close> F show False
    3.39 +        by auto
    3.40 +    qed }
    3.41 +  note * = this
    3.42 +
    3.43 +  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
    3.44 +    unfolding Limsup_def INF_def
    3.45 +    by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
    3.46 +       (auto intro: eventually_True)
    3.47 +  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
    3.48 +    by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
    3.49 +       (auto dest!: eventually_happens simp: F)
    3.50 +  finally show ?thesis
    3.51 +    by (auto simp: Liminf_def)
    3.52 +qed
    3.53 +
    3.54  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 24 15:21:12 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Sep 25 16:54:31 2015 +0200
     4.3 @@ -2200,18 +2200,35 @@
     4.4  
     4.5  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
     4.6  
     4.7 -lemma vector_derivative_unique_at:
     4.8 -  assumes "(f has_vector_derivative f') (at x)"
     4.9 -    and "(f has_vector_derivative f'') (at x)"
    4.10 +lemma vector_derivative_unique_within:
    4.11 +  assumes not_bot: "at x within s \<noteq> bot"
    4.12 +    and f': "(f has_vector_derivative f') (at x within s)"
    4.13 +    and f'': "(f has_vector_derivative f'') (at x within s)"
    4.14    shows "f' = f''"
    4.15  proof -
    4.16    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
    4.17 -    using assms [unfolded has_vector_derivative_def]
    4.18 -    by (rule frechet_derivative_unique_at)
    4.19 +  proof (rule frechet_derivative_unique_within)
    4.20 +    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
    4.21 +    proof clarsimp
    4.22 +      fix e :: real assume "0 < e"
    4.23 +      with islimpt_approachable_real[of x s] not_bot
    4.24 +      obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
    4.25 +        by (auto simp add: trivial_limit_within)
    4.26 +      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
    4.27 +        by (intro exI[of _ "x' - x"]) auto
    4.28 +    qed
    4.29 +  qed (insert f' f'', auto simp: has_vector_derivative_def)
    4.30    then show ?thesis
    4.31      unfolding fun_eq_iff by auto
    4.32  qed
    4.33  
    4.34 +lemma vector_derivative_unique_at:
    4.35 +  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f'') (at x) \<Longrightarrow> f' = f''"
    4.36 +  by (rule vector_derivative_unique_within) auto
    4.37 +
    4.38 +lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
    4.39 +  by (auto simp: differentiable_def has_vector_derivative_def)
    4.40 +
    4.41  lemma vector_derivative_works:
    4.42    "f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
    4.43      (is "?l = ?r")
    4.44 @@ -2226,38 +2243,44 @@
    4.45      by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
    4.46  qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
    4.47  
    4.48 +lemma vector_derivative_within:
    4.49 +  assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
    4.50 +  shows "vector_derivative f (at x within s) = y"
    4.51 +  using y
    4.52 +  by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
    4.53 +     (auto simp: differentiable_def has_vector_derivative_def)
    4.54 +
    4.55 +lemma islimpt_closure_open:
    4.56 +  fixes s :: "'a::perfect_space set"
    4.57 +  assumes "open s" and t: "t = closure s" "x \<in> t"
    4.58 +  shows "x islimpt t"
    4.59 +proof cases
    4.60 +  assume "x \<in> s" 
    4.61 +  { fix T assume "x \<in> T" "open T"
    4.62 +    then have "open (s \<inter> T)"
    4.63 +      using \<open>open s\<close> by auto
    4.64 +    then have "s \<inter> T \<noteq> {x}"
    4.65 +      using not_open_singleton[of x] by auto
    4.66 +    with \<open>x \<in> T\<close> \<open>x \<in> s\<close> have "\<exists>y\<in>t. y \<in> T \<and> y \<noteq> x"
    4.67 +      using closure_subset[of s] by (auto simp: t) }
    4.68 +  then show ?thesis
    4.69 +    by (auto intro!: islimptI)
    4.70 +next
    4.71 +  assume "x \<notin> s" with t show ?thesis
    4.72 +    unfolding t closure_def by (auto intro: islimpt_subset)
    4.73 +qed
    4.74 +
    4.75  lemma vector_derivative_unique_within_closed_interval:
    4.76 -  assumes "a < b"
    4.77 -    and "x \<in> cbox a b"
    4.78 -  assumes "(f has_vector_derivative f') (at x within cbox a b)"
    4.79 -  assumes "(f has_vector_derivative f'') (at x within cbox a b)"
    4.80 +  assumes ab: "a < b" "x \<in> cbox a b"
    4.81 +  assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)"
    4.82    shows "f' = f''"
    4.83 -proof -
    4.84 -  have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
    4.85 -    apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
    4.86 -    using assms(3-)[unfolded has_vector_derivative_def]
    4.87 -    using assms(1-2)
    4.88 -    apply auto
    4.89 -    done
    4.90 -  show ?thesis
    4.91 -  proof (rule ccontr)
    4.92 -    assume **: "f' \<noteq> f''"
    4.93 -    with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
    4.94 -      by (auto simp: fun_eq_iff)
    4.95 -    with ** show False
    4.96 -      unfolding o_def by auto
    4.97 -  qed
    4.98 -qed
    4.99 +  using ab
   4.100 +  by (intro vector_derivative_unique_within[OF _ D])
   4.101 +     (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"])
   4.102  
   4.103  lemma vector_derivative_at:
   4.104    "(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
   4.105 -  apply (rule vector_derivative_unique_at)
   4.106 -  defer
   4.107 -  apply assumption
   4.108 -  unfolding vector_derivative_works[symmetric] differentiable_def
   4.109 -  unfolding has_vector_derivative_def
   4.110 -  apply auto
   4.111 -  done
   4.112 +  by (intro vector_derivative_within at_neq_bot)
   4.113  
   4.114  lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
   4.115    by (simp add: vector_derivative_at)
   4.116 @@ -2292,15 +2315,12 @@
   4.117  done
   4.118  
   4.119  lemma vector_derivative_within_closed_interval:
   4.120 -  assumes "a < b"
   4.121 -    and "x \<in> cbox a b"
   4.122 -  assumes "(f has_vector_derivative f') (at x within cbox a b)"
   4.123 +  assumes ab: "a < b" "x \<in> cbox a b"
   4.124 +  assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
   4.125    shows "vector_derivative f (at x within cbox a b) = f'"
   4.126 -  apply (rule vector_derivative_unique_within_closed_interval)
   4.127 -  using vector_derivative_works[unfolded differentiable_def]
   4.128 -  using assms
   4.129 -  apply (auto simp add:has_vector_derivative_def)
   4.130 -  done
   4.131 +  by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
   4.132 +            vector_derivative_works[THEN iffD1] differentiableI_vector)
   4.133 +     fact
   4.134  
   4.135  lemma has_vector_derivative_within_subset:
   4.136    "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
     5.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Sep 24 15:21:12 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Sep 25 16:54:31 2015 +0200
     5.3 @@ -313,6 +313,46 @@
     5.4    apply (metis INF_absorb centre_in_ball)
     5.5    done
     5.6  
     5.7 +lemma continuous_on_inverse_ereal: "continuous_on {0::ereal ..} inverse"
     5.8 +  unfolding continuous_on_def
     5.9 +proof clarsimp
    5.10 +  fix x :: ereal assume "0 \<le> x"
    5.11 +  moreover have "at 0 within {0 ..} = at_right (0::ereal)"
    5.12 +    by (auto simp: filter_eq_iff eventually_at_filter le_less)
    5.13 +  moreover have "0 < x \<Longrightarrow> at x within {0 ..} = at x"
    5.14 +    using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \<infinity>"])
    5.15 +  ultimately show "(inverse ---> inverse x) (at x within {0..})"
    5.16 +    by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
    5.17 +qed
    5.18 +
    5.19 +
    5.20 +lemma Liminf_inverse_ereal:
    5.21 +  assumes nneg: "\<forall>\<^sub>F x in F. f x \<ge> (0 :: ereal)" and "F \<noteq> bot"
    5.22 +  shows "Liminf F (\<lambda>n. inverse (f n)) = inverse (Limsup F f)"
    5.23 +proof -
    5.24 +  def I \<equiv> "\<lambda>x::ereal. if x \<le> 0 then \<infinity> else inverse x"
    5.25 +  have "Liminf F (\<lambda>n. I (f n)) = I (Limsup F f)"
    5.26 +  proof (rule Liminf_compose_continuous_antimono)
    5.27 +    have "continuous_on ({.. 0} \<union> {0 ..}) I"
    5.28 +      unfolding I_def by (intro continuous_on_cases) (auto intro: continuous_on_const continuous_on_inverse_ereal)
    5.29 +    also have "{.. 0} \<union> {0::ereal ..} = UNIV"
    5.30 +      by auto
    5.31 +    finally show "continuous_on UNIV I" .
    5.32 +    show "antimono I"
    5.33 +      unfolding antimono_def I_def by (auto intro: ereal_inverse_antimono)
    5.34 +  qed fact
    5.35 +  also have "Liminf F (\<lambda>n. I (f n)) = Liminf F (\<lambda>n. inverse (f n))"
    5.36 +  proof (rule Liminf_eq)
    5.37 +    show "\<forall>\<^sub>F x in F. I (f x) = inverse (f x)"
    5.38 +      using nneg by eventually_elim (auto simp: I_def)
    5.39 +  qed
    5.40 +  also have "0 \<le> Limsup F f"
    5.41 +    by (intro le_Limsup) fact+
    5.42 +  then have "I (Limsup F f) = inverse (Limsup F f)"
    5.43 +    by (auto simp: I_def)
    5.44 +  finally show ?thesis .
    5.45 +qed
    5.46 +
    5.47  subsection \<open>monoset\<close>
    5.48  
    5.49  definition (in order) mono_set:
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 24 15:21:12 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 25 16:54:31 2015 +0200
     6.3 @@ -1551,6 +1551,43 @@
     6.4    qed
     6.5  qed
     6.6  
     6.7 +lemma interior_Ici:
     6.8 +  fixes x :: "'a :: {dense_linorder, linorder_topology}"
     6.9 +  assumes "b < x"
    6.10 +  shows "interior { x ..} = { x <..}"
    6.11 +proof (rule interior_unique)
    6.12 +  fix T assume "T \<subseteq> {x ..}" "open T"
    6.13 +  moreover have "x \<notin> T"
    6.14 +  proof
    6.15 +    assume "x \<in> T"
    6.16 +    obtain y where "y < x" "{y <.. x} \<subseteq> T"
    6.17 +      using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
    6.18 +    with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
    6.19 +      by (auto simp: subset_eq Ball_def)
    6.20 +    with \<open>T \<subseteq> {x ..}\<close> show False by auto
    6.21 +  qed
    6.22 +  ultimately show "T \<subseteq> {x <..}"
    6.23 +    by (auto simp: subset_eq less_le)
    6.24 +qed auto
    6.25 +
    6.26 +lemma interior_Iic:
    6.27 +  fixes x :: "'a :: {dense_linorder, linorder_topology}"
    6.28 +  assumes "x < b"
    6.29 +  shows "interior {.. x} = {..< x}"
    6.30 +proof (rule interior_unique)
    6.31 +  fix T assume "T \<subseteq> {.. x}" "open T"
    6.32 +  moreover have "x \<notin> T"
    6.33 +  proof
    6.34 +    assume "x \<in> T"
    6.35 +    obtain y where "x < y" "{x ..< y} \<subseteq> T"
    6.36 +      using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
    6.37 +    with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
    6.38 +      by (auto simp: subset_eq Ball_def less_le)
    6.39 +    with \<open>T \<subseteq> {.. x}\<close> show False by auto
    6.40 +  qed
    6.41 +  ultimately show "T \<subseteq> {..< x}"
    6.42 +    by (auto simp: subset_eq less_le)
    6.43 +qed auto
    6.44  
    6.45  subsection \<open>Closure of a Set\<close>
    6.46  
    6.47 @@ -1763,10 +1800,6 @@
    6.48  
    6.49  text \<open>Some property holds "sufficiently close" to the limit point.\<close>
    6.50  
    6.51 -lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
    6.52 -  unfolding trivial_limit_def
    6.53 -  by (auto elim: eventually_rev_mp)
    6.54 -
    6.55  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
    6.56    by simp
    6.57  
     7.1 --- a/src/HOL/Topological_Spaces.thy	Thu Sep 24 15:21:12 2015 +0200
     7.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Sep 25 16:54:31 2015 +0200
     7.3 @@ -381,6 +381,17 @@
     7.4    "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
     7.5    by (simp only: at_within_open)
     7.6  
     7.7 +lemma at_within_nhd:
     7.8 +  assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
     7.9 +  shows "at x within T = at x within U"
    7.10 +  unfolding filter_eq_iff eventually_at_filter
    7.11 +proof (intro allI eventually_subst)
    7.12 +  have "eventually (\<lambda>x. x \<in> S) (nhds x)"
    7.13 +    using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
    7.14 +  then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P  
    7.15 +    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
    7.16 +qed
    7.17 +
    7.18  lemma at_within_empty [simp]: "at a within {} = bot"
    7.19    unfolding at_within_def by simp
    7.20  
    7.21 @@ -1574,7 +1585,7 @@
    7.22    "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
    7.23    by (simp add: continuous_within filterlim_at_split)
    7.24  
    7.25 -subsubsection\<open>Open-cover compactness\<close>
    7.26 +subsubsection \<open>Open-cover compactness\<close>
    7.27  
    7.28  context topological_space
    7.29  begin