src/HOL/Topological_Spaces.thy
changeset 65204 d23eded35a33
parent 65036 ab7e11730ad8
child 65583 8d53b3bebab4
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sun Mar 12 19:06:10 2017 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 10 23:16:40 2017 +0100
     1.3 @@ -150,12 +150,12 @@
     1.4  instance t1_space \<subseteq> t0_space
     1.5    by standard (fast dest: t1_space)
     1.6  
     1.7 +context t1_space begin
     1.8 +
     1.9  lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
    1.10 -  for x y :: "'a::t1_space"
    1.11    using t1_space[of x y] by blast
    1.12  
    1.13  lemma closed_singleton [iff]: "closed {a}"
    1.14 -  for a :: "'a::t1_space"
    1.15  proof -
    1.16    let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
    1.17    have "open ?T"
    1.18 @@ -167,7 +167,6 @@
    1.19  qed
    1.20  
    1.21  lemma closed_insert [continuous_intros, simp]:
    1.22 -  fixes a :: "'a::t1_space"
    1.23    assumes "closed S"
    1.24    shows "closed (insert a S)"
    1.25  proof -
    1.26 @@ -178,9 +177,9 @@
    1.27  qed
    1.28  
    1.29  lemma finite_imp_closed: "finite S \<Longrightarrow> closed S"
    1.30 -  for S :: "'a::t1_space set"
    1.31    by (induct pred: finite) simp_all
    1.32  
    1.33 +end
    1.34  
    1.35  text \<open>T2 spaces are also known as Hausdorff spaces.\<close>
    1.36  
    1.37 @@ -190,12 +189,10 @@
    1.38  instance t2_space \<subseteq> t1_space
    1.39    by standard (fast dest: hausdorff)
    1.40  
    1.41 -lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
    1.42 -  for x y :: "'a::t2_space"
    1.43 +lemma (in t2_space) separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
    1.44    using hausdorff [of x y] by blast
    1.45  
    1.46 -lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
    1.47 -  for x y :: "'a::t0_space"
    1.48 +lemma (in t0_space) separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
    1.49    using t0_space [of x y] by blast
    1.50  
    1.51  
    1.52 @@ -204,9 +201,9 @@
    1.53  class perfect_space = topological_space +
    1.54    assumes not_open_singleton: "\<not> open {x}"
    1.55  
    1.56 -lemma UNIV_not_singleton: "UNIV \<noteq> {x}"
    1.57 -  for x :: "'a::perfect_space"
    1.58 -  by (metis open_UNIV not_open_singleton)
    1.59 +lemma (in perfect_space) UNIV_not_singleton: "UNIV \<noteq> {x}"
    1.60 +  for x::'a
    1.61 +  by (metis (no_types) open_UNIV not_open_singleton)
    1.62  
    1.63  
    1.64  subsection \<open>Generators for toplogies\<close>
    1.65 @@ -476,10 +473,10 @@
    1.66    "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
    1.67    by (subst eventually_nhds) blast
    1.68  
    1.69 -lemma eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
    1.70 +lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
    1.71    by (subst (asm) eventually_nhds) blast
    1.72  
    1.73 -lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    1.74 +lemma (in topological_space) nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    1.75    by (simp add: trivial_limit_def eventually_nhds)
    1.76  
    1.77  lemma (in t1_space) t1_space_nhds: "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
    1.78 @@ -494,28 +491,34 @@
    1.79  lemma (in discrete_topology) at_discrete: "at x within S = bot"
    1.80    unfolding at_within_def nhds_discrete by simp
    1.81  
    1.82 -lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    1.83 +lemma (in topological_space) at_within_eq:
    1.84 +  "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    1.85    unfolding nhds_def at_within_def
    1.86    by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
    1.87  
    1.88 -lemma eventually_at_filter:
    1.89 +lemma (in topological_space) eventually_at_filter:
    1.90    "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
    1.91    by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)
    1.92  
    1.93 -lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
    1.94 +lemma (in topological_space) at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
    1.95    unfolding at_within_def by (intro inf_mono) auto
    1.96  
    1.97 -lemma eventually_at_topological:
    1.98 +lemma (in topological_space) eventually_at_topological:
    1.99    "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
   1.100    by (simp add: eventually_nhds eventually_at_filter)
   1.101  
   1.102 -lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   1.103 +lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   1.104    unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
   1.105  
   1.106 -lemma at_within_open_NO_MATCH: "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
   1.107 +lemma (in topological_space) at_within_open_NO_MATCH:
   1.108 +  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
   1.109    by (simp only: at_within_open)
   1.110  
   1.111 -lemma at_within_nhd:
   1.112 +lemma (in topological_space) at_within_open_subset:
   1.113 +  "a \<in> S \<Longrightarrow> open S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> at a within T = at a"
   1.114 +  by (metis at_le at_within_open dual_order.antisym subset_UNIV)
   1.115 +
   1.116 +lemma (in topological_space) at_within_nhd:
   1.117    assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
   1.118    shows "at x within T = at x within U"
   1.119    unfolding filter_eq_iff eventually_at_filter
   1.120 @@ -526,14 +529,15 @@
   1.121      by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
   1.122  qed
   1.123  
   1.124 -lemma at_within_empty [simp]: "at a within {} = bot"
   1.125 +lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
   1.126    unfolding at_within_def by simp
   1.127  
   1.128 -lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
   1.129 +lemma (in topological_space) at_within_union:
   1.130 +  "at x within (S \<union> T) = sup (at x within S) (at x within T)"
   1.131    unfolding filter_eq_iff eventually_sup eventually_at_filter
   1.132    by (auto elim!: eventually_rev_mp)
   1.133  
   1.134 -lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   1.135 +lemma (in topological_space) at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   1.136    unfolding trivial_limit_def eventually_at_topological
   1.137    apply safe
   1.138     apply (case_tac "S = {a}")
   1.139 @@ -542,8 +546,7 @@
   1.140    apply fast
   1.141    done
   1.142  
   1.143 -lemma at_neq_bot [simp]: "at a \<noteq> bot"
   1.144 -  for a :: "'a::perfect_space"
   1.145 +lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
   1.146    by (simp add: at_eq_bot_iff not_open_singleton)
   1.147  
   1.148  lemma (in order_topology) nhds_order:
   1.149 @@ -556,7 +559,7 @@
   1.150      by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
   1.151  qed
   1.152  
   1.153 -lemma filterlim_at_within_If:
   1.154 +lemma (in topological_space) filterlim_at_within_If:
   1.155    assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
   1.156      and "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
   1.157    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x within A)"
   1.158 @@ -580,7 +583,7 @@
   1.159    finally show "filterlim g G (inf (at x within A) (principal {x. \<not> P x}))" .
   1.160  qed
   1.161  
   1.162 -lemma filterlim_at_If:
   1.163 +lemma (in topological_space) filterlim_at_If:
   1.164    assumes "filterlim f G (at x within {x. P x})"
   1.165      and "filterlim g G (at x within {x. \<not>P x})"
   1.166    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
   1.167 @@ -641,22 +644,20 @@
   1.168    using gt_ex[of x]
   1.169    by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
   1.170  
   1.171 -lemma at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
   1.172 -  for x :: "'a::linorder_topology"
   1.173 +lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
   1.174    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
   1.175        elim: eventually_elim2 eventually_mono)
   1.176  
   1.177 -lemma eventually_at_split:
   1.178 +lemma (in linorder_topology) eventually_at_split:
   1.179    "eventually P (at x) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   1.180 -  for x :: "'a::linorder_topology"
   1.181    by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   1.182  
   1.183 -lemma eventually_at_leftI:
   1.184 +lemma (in order_topology) eventually_at_leftI:
   1.185    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
   1.186    shows   "eventually P (at_left b)"
   1.187    using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto
   1.188  
   1.189 -lemma eventually_at_rightI:
   1.190 +lemma (in order_topology) eventually_at_rightI:
   1.191    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
   1.192    shows   "eventually P (at_right a)"
   1.193    using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
   1.194 @@ -671,7 +672,7 @@
   1.195  definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
   1.196    where "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
   1.197  
   1.198 -lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
   1.199 +lemma (in topological_space) tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
   1.200    by simp
   1.201  
   1.202  named_theorems tendsto_intros "introduction rules for tendsto"
   1.203 @@ -682,7 +683,9 @@
   1.204        |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
   1.205  \<close>
   1.206  
   1.207 -lemma (in topological_space) tendsto_def:
   1.208 +context topological_space begin
   1.209 +
   1.210 +lemma tendsto_def:
   1.211     "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   1.212     unfolding nhds_def filterlim_INF filterlim_principal by auto
   1.213  
   1.214 @@ -692,14 +695,17 @@
   1.215  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
   1.216    unfolding tendsto_def le_filter_def by fast
   1.217  
   1.218 -lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
   1.219 -  by (blast intro: tendsto_mono at_le)
   1.220 -
   1.221 -lemma filterlim_at:
   1.222 +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
   1.223 +  by (auto simp: tendsto_def eventually_at_topological)
   1.224 +
   1.225 +lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   1.226 +  by (simp add: tendsto_def)
   1.227 +
   1.228 +lemma  filterlim_at:
   1.229    "(LIM x F. f x :> at b within s) \<longleftrightarrow> eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F"
   1.230    by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
   1.231  
   1.232 -lemma filterlim_at_withinI:
   1.233 +lemma  filterlim_at_withinI:
   1.234    assumes "filterlim f (nhds c) F"
   1.235    assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"
   1.236    shows   "filterlim f (at c within A) F"
   1.237 @@ -711,14 +717,23 @@
   1.238    shows   "filterlim f (at c) F"
   1.239    using assms by (intro filterlim_at_withinI) simp_all
   1.240  
   1.241 -lemma (in topological_space) topological_tendstoI:
   1.242 +lemma topological_tendstoI:
   1.243    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
   1.244    by (auto simp: tendsto_def)
   1.245  
   1.246 -lemma (in topological_space) topological_tendstoD:
   1.247 +lemma topological_tendstoD:
   1.248    "(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   1.249    by (auto simp: tendsto_def)
   1.250  
   1.251 +lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
   1.252 +  by (simp add: tendsto_def)
   1.253 +
   1.254 +end
   1.255 +
   1.256 +lemma tendsto_within_subset:
   1.257 +  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
   1.258 +  by (blast intro: tendsto_mono at_le)
   1.259 +
   1.260  lemma (in order_topology) order_tendsto_iff:
   1.261    "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
   1.262    by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)
   1.263 @@ -734,9 +749,6 @@
   1.264      and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
   1.265    using assms by (auto simp: order_tendsto_iff)
   1.266  
   1.267 -lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
   1.268 -  by (simp add: tendsto_def)
   1.269 -
   1.270  lemma (in linorder_topology) tendsto_max:
   1.271    assumes X: "(X \<longlongrightarrow> x) net"
   1.272      and Y: "(Y \<longlongrightarrow> y) net"
   1.273 @@ -773,11 +785,18 @@
   1.274      by (auto simp: min_less_iff_disj elim: eventually_mono)
   1.275  qed
   1.276  
   1.277 -lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
   1.278 -  by (auto simp: tendsto_def eventually_at_topological)
   1.279 -
   1.280 -lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   1.281 -  by (simp add: tendsto_def)
   1.282 +lemma (in order_topology)
   1.283 +  assumes "a < b"
   1.284 +  shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
   1.285 +    and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
   1.286 +  using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
   1.287 +  using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
   1.288 +  by (auto intro!: order_class.antisym filter_leI
   1.289 +      simp: eventually_at_filter less_le
   1.290 +      elim: eventually_elim2)
   1.291 +
   1.292 +lemma (in order_topology) at_within_Icc_at: "a < x \<Longrightarrow> x < b \<Longrightarrow> at x within {a..b} = at x"
   1.293 +  by (rule at_within_open_subset[where S="{a<..<b}"]) auto
   1.294  
   1.295  lemma (in t2_space) tendsto_unique:
   1.296    assumes "F \<noteq> bot"
   1.297 @@ -810,22 +829,19 @@
   1.298    shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   1.299    by (auto intro!: tendsto_unique [OF assms tendsto_const])
   1.300  
   1.301 -lemma increasing_tendsto:
   1.302 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.303 +lemma (in order_topology) increasing_tendsto:
   1.304    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   1.305      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   1.306    shows "(f \<longlongrightarrow> l) F"
   1.307    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   1.308  
   1.309 -lemma decreasing_tendsto:
   1.310 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.311 +lemma (in order_topology) decreasing_tendsto:
   1.312    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
   1.313      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   1.314    shows "(f \<longlongrightarrow> l) F"
   1.315    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   1.316  
   1.317 -lemma tendsto_sandwich:
   1.318 -  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   1.319 +lemma (in order_topology) tendsto_sandwich:
   1.320    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
   1.321    assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
   1.322    shows "(g \<longlongrightarrow> c) net"
   1.323 @@ -839,8 +855,7 @@
   1.324      using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
   1.325  qed
   1.326  
   1.327 -lemma limit_frequently_eq:
   1.328 -  fixes c d :: "'a::t1_space"
   1.329 +lemma (in t1_space) limit_frequently_eq:
   1.330    assumes "F \<noteq> bot"
   1.331      and "frequently (\<lambda>x. f x = c) F"
   1.332      and "(f \<longlongrightarrow> d) F"
   1.333 @@ -857,8 +872,7 @@
   1.334      unfolding frequently_def by contradiction
   1.335  qed
   1.336  
   1.337 -lemma tendsto_imp_eventually_ne:
   1.338 -  fixes c :: "'a::t1_space"
   1.339 +lemma (in t1_space) tendsto_imp_eventually_ne:
   1.340    assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
   1.341    shows "eventually (\<lambda>z. f z \<noteq> c') F"
   1.342  proof (cases "F=bot")
   1.343 @@ -876,8 +890,7 @@
   1.344    qed
   1.345  qed
   1.346  
   1.347 -lemma tendsto_le:
   1.348 -  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   1.349 +lemma (in linorder_topology) tendsto_le:
   1.350    assumes F: "\<not> trivial_limit F"
   1.351      and x: "(f \<longlongrightarrow> x) F"
   1.352      and y: "(g \<longlongrightarrow> y) F"
   1.353 @@ -895,16 +908,14 @@
   1.354      by (simp add: eventually_False)
   1.355  qed
   1.356  
   1.357 -lemma tendsto_lowerbound:
   1.358 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.359 +lemma (in linorder_topology) tendsto_lowerbound:
   1.360    assumes x: "(f \<longlongrightarrow> x) F"
   1.361        and ev: "eventually (\<lambda>i. a \<le> f i) F"
   1.362        and F: "\<not> trivial_limit F"
   1.363    shows "a \<le> x"
   1.364    using F x tendsto_const ev by (rule tendsto_le)
   1.365  
   1.366 -lemma tendsto_upperbound:
   1.367 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.368 +lemma (in linorder_topology) tendsto_upperbound:
   1.369    assumes x: "(f \<longlongrightarrow> x) F"
   1.370        and ev: "eventually (\<lambda>i. a \<ge> f i) F"
   1.371        and F: "\<not> trivial_limit F"
   1.372 @@ -1840,7 +1851,8 @@
   1.373    unfolding continuous_on_def by auto
   1.374  
   1.375  lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
   1.376 -  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
   1.377 +  unfolding continuous_on_def
   1.378 +  by (metis subset_eq tendsto_within_subset)
   1.379  
   1.380  lemma continuous_on_compose[continuous_intros]:
   1.381    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g \<circ> f)"
   1.382 @@ -1912,6 +1924,25 @@
   1.383         (auto intro: less_le_trans[OF _ mono] less_imp_le)
   1.384  qed
   1.385  
   1.386 +lemma continuous_on_IccI:
   1.387 +  "\<lbrakk>(f \<longlongrightarrow> f a) (at_right a);
   1.388 +    (f \<longlongrightarrow> f b) (at_left b);
   1.389 +    (\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> f \<midarrow>x\<rightarrow> f x); a < b\<rbrakk> \<Longrightarrow>
   1.390 +    continuous_on {a .. b} f"
   1.391 +  for a::"'a::linorder_topology"
   1.392 +  using at_within_open[of _ "{a<..<b}"]
   1.393 +  by (auto simp: continuous_on_def at_within_Icc_at_right at_within_Icc_at_left le_less
   1.394 +      at_within_Icc_at)
   1.395 +
   1.396 +lemma
   1.397 +  fixes a b::"'a::linorder_topology"
   1.398 +  assumes "continuous_on {a .. b} f" "a < b"
   1.399 +  shows continuous_on_Icc_at_rightD: "(f \<longlongrightarrow> f a) (at_right a)"
   1.400 +    and continuous_on_Icc_at_leftD: "(f \<longlongrightarrow> f b) (at_left b)"
   1.401 +  using assms
   1.402 +  by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
   1.403 +      dest: bspec[where x=a] bspec[where x=b])
   1.404 +
   1.405  
   1.406  subsubsection \<open>Continuity at a point\<close>
   1.407