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.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.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
```