--- a/src/HOL/Deriv.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 21 19:52:13 2015 +0100
@@ -644,6 +644,18 @@
((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
by (auto simp: has_vector_derivative_def scaleR_diff_right)
+lemma has_vector_derivative_add_const:
+ "((\<lambda>t. g t + z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+apply (intro iffI)
+apply (drule has_vector_derivative_diff [where g = "\<lambda>t. z", OF _ has_vector_derivative_const], simp)
+apply (drule has_vector_derivative_add [OF _ has_vector_derivative_const], simp)
+done
+
+lemma has_vector_derivative_diff_const:
+ "((\<lambda>t. g t - z) has_vector_derivative f') (at x) = ((\<lambda>t. g t) has_vector_derivative f') (at x)"
+using has_vector_derivative_add_const [where z = "-z"]
+by simp
+
lemma (in bounded_linear) has_vector_derivative:
assumes "(g has_vector_derivative g') F"
shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
--- a/src/HOL/Fun.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Fun.thy Mon Sep 21 19:52:13 2015 +0100
@@ -69,7 +69,7 @@
lemma comp_eq_elim:
"a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
- by (simp add: fun_eq_iff)
+ by (simp add: fun_eq_iff)
lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
by clarsimp
@@ -833,7 +833,7 @@
thus False by best
qed
-subsection \<open>Setup\<close>
+subsection \<open>Setup\<close>
subsubsection \<open>Proof tools\<close>
--- a/src/HOL/Int.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Int.thy Mon Sep 21 19:52:13 2015 +0100
@@ -518,7 +518,7 @@
lemma int_cases3 [case_names zero pos neg]:
fixes k :: int
assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
- and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
+ and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
shows "P"
proof (cases k "0::int" rule: linorder_cases)
case equal with assms(1) show P by simp
@@ -890,7 +890,7 @@
moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
using that by induct simp
ultimately show ?thesis by blast
-qed
+qed
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
apply (rule sym)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Sep 21 19:52:13 2015 +0100
@@ -4,58 +4,6 @@
imports Complex_Transcendental Weierstrass
begin
-(*FIXME migrate into libraries*)
-
-lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
- by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
-
-lemma continuous_on_strong_cong:
- "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
- by (simp add: simp_implies_def)
-
-thm image_affinity_atLeastAtMost_div_diff
-lemma image_affinity_atLeastAtMost_div:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {a/m + c .. b/m + c}
- else {b/m + c .. a/m + c})"
- using image_affinity_atLeastAtMost [of "inverse m" c a b]
- by (simp add: field_class.field_divide_inverse algebra_simps)
-
-thm continuous_on_closed_Un
-lemma continuous_on_open_Un:
- "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
- using continuous_on_open_Union [of "{s,t}"] by auto
-
-thm continuous_on_eq (*REPLACE*)
-lemma continuous_on_eq:
- "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
- unfolding continuous_on_def tendsto_def eventually_at_topological
- by simp
-
-thm vector_derivative_add_at
-lemma vector_derivative_mult_at [simp]:
- fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
- shows "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
- \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
- by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
-
-lemma vector_derivative_scaleR_at [simp]:
- "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
- \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
-apply (rule vector_derivative_at)
-apply (rule has_vector_derivative_scaleR)
-apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
-done
-
-thm Derivative.vector_diff_chain_at
-lemma vector_derivative_chain_at:
- assumes "f differentiable at x" "(g differentiable at (f x))"
- shows "vector_derivative (g \<circ> f) (at x) =
- vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
-by (metis Derivative.vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
-
-
subsection \<open>Piecewise differentiable functions\<close>
definition piecewise_differentiable_on
@@ -89,6 +37,9 @@
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
intro: differentiable_within_subset)
+lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
+ by (simp add: differentiable_imp_piecewise_differentiable)
+
lemma piecewise_differentiable_compose:
"\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
\<And>x. finite (s \<inter> f-`{x})\<rbrakk>
@@ -466,7 +417,7 @@
by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add)
qed
-lemma piecewise_C1_differentiable_C1_diff:
+lemma piecewise_C1_differentiable_diff:
"\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on s\<rbrakk>
\<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on s"
unfolding diff_conv_add_uminus
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 21 19:52:13 2015 +0100
@@ -2277,6 +2277,20 @@
\<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
+lemma vector_derivative_mult_at [simp]:
+ fixes f g :: "real \<Rightarrow> 'a :: real_normed_algebra"
+ shows "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a"
+ by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric])
+
+lemma vector_derivative_scaleR_at [simp]:
+ "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+ \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
+apply (rule vector_derivative_at)
+apply (rule has_vector_derivative_scaleR)
+apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
+done
+
lemma vector_derivative_within_closed_interval:
assumes "a < b"
and "x \<in> cbox a b"
@@ -2356,4 +2370,10 @@
a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+lemma vector_derivative_chain_at:
+ assumes "f differentiable at x" "(g differentiable at (f x))"
+ shows "vector_derivative (g \<circ> f) (at x) =
+ vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
+by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
+
end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 21 19:52:13 2015 +0100
@@ -496,6 +496,9 @@
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
+lemma abs_eq_content: "abs (y - x) = (if x\<le>y then content {x .. y} else content {y..x})"
+ by (auto simp: content_real)
+
lemma content_singleton[simp]: "content {a} = 0"
proof -
have "content (cbox a a) = 0"
@@ -6414,133 +6417,75 @@
apply (rule has_integral_const)
done
+lemma integral_has_vector_derivative_continuous_at:
+ fixes f :: "real \<Rightarrow> 'a::banach"
+ assumes f: "f integrable_on {a..b}"
+ and x: "x \<in> {a..b}"
+ and fx: "continuous (at x within {a..b}) f"
+ shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
+proof -
+ let ?I = "\<lambda>a b. integral {a..b} f"
+ { fix e::real
+ assume "e > 0"
+ obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
+ using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
+ have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+ if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y
+ proof (cases "y < x")
+ case False
+ have "f integrable_on {a..y}"
+ using f y by (simp add: integrable_subinterval_real)
+ then have Idiff: "?I a y - ?I a x = ?I x y"
+ using False x by (simp add: algebra_simps integral_combine)
+ have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
+ apply (rule has_integral_sub)
+ using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+ using has_integral_const_real [of "f x" x y] False
+ apply (simp add: )
+ done
+ show ?thesis
+ using False
+ apply (simp add: abs_eq_content del: content_real_if)
+ apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
+ using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
+ done
+ next
+ case True
+ have "f integrable_on {a..x}"
+ using f x by (simp add: integrable_subinterval_real)
+ then have Idiff: "?I a x - ?I a y = ?I y x"
+ using True x y by (simp add: algebra_simps integral_combine)
+ have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
+ apply (rule has_integral_sub)
+ using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+ using has_integral_const_real [of "f x" y x] True
+ apply (simp add: )
+ done
+ have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+ using True
+ apply (simp add: abs_eq_content del: content_real_if)
+ apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
+ using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
+ done
+ then show ?thesis
+ by (simp add: algebra_simps norm_minus_commute)
+ qed
+ then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+ using `d>0` by blast
+ }
+ then show ?thesis
+ by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
+qed
+
lemma integral_has_vector_derivative:
fixes f :: "real \<Rightarrow> 'a::banach"
assumes "continuous_on {a .. b} f"
and "x \<in> {a .. b}"
shows "((\<lambda>u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b})"
- unfolding has_vector_derivative_def has_derivative_within_alt
- apply safe
- apply (rule bounded_linear_scaleR_left)
-proof -
- fix e :: real
- assume e: "e > 0"
- note compact_uniformly_continuous[OF assms(1) compact_Icc,unfolded uniformly_continuous_on_def]
- from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format]
- let ?I = "\<lambda>a b. integral {a .. b} f"
- show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
- norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
- proof (rule, rule, rule d, safe, goal_cases)
- case prems: (1 y)
- show ?case
- proof (cases "y < x")
- case False
- have "f integrable_on {a .. y}"
- apply (rule integrable_subinterval_real,rule integrable_continuous_real)
- apply (rule assms)
- unfolding not_less
- using assms(2) prems
- apply auto
- done
- then have *: "?I a y - ?I a x = ?I x y"
- unfolding algebra_simps
- apply (subst eq_commute)
- apply (rule integral_combine)
- using False
- unfolding not_less
- using assms(2) prems
- apply auto
- done
- have **: "norm (y - x) = content {x .. y}"
- using False by (auto simp: content_real)
- show ?thesis
- unfolding **
- apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
- unfolding *
- defer
- apply (rule has_integral_sub)
- apply (rule integrable_integral)
- apply (rule integrable_subinterval_real)
- apply (rule integrable_continuous_real)
- apply (rule assms)+
- proof -
- show "{x .. y} \<subseteq> {a .. b}"
- using prems assms(2) by auto
- have *: "y - x = norm (y - x)"
- using False by auto
- show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x .. y}"
- apply (subst *)
- unfolding **
- by blast
- show "\<forall>xa\<in>{x .. y}. norm (f xa - f x) \<le> e"
- apply safe
- apply (rule less_imp_le)
- apply (rule d(2)[unfolded dist_norm])
- using assms(2)
- using prems
- apply auto
- done
- qed (insert e, auto)
- next
- case True
- have "f integrable_on cbox a x"
- apply (rule integrable_subinterval,rule integrable_continuous)
- unfolding box_real
- apply (rule assms)+
- unfolding not_less
- using assms(2) prems
- apply auto
- done
- then have *: "?I a x - ?I a y = ?I y x"
- unfolding algebra_simps
- apply (subst eq_commute)
- apply (rule integral_combine)
- using True using assms(2) prems
- apply auto
- done
- have **: "norm (y - x) = content {y .. x}"
- apply (subst content_real)
- using True
- unfolding not_less
- apply auto
- done
- have ***: "\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)"
- unfolding scaleR_left.diff by auto
- show ?thesis
- apply (subst ***)
- unfolding norm_minus_cancel **
- apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
- unfolding *
- unfolding o_def
- defer
- apply (rule has_integral_sub)
- apply (subst minus_minus[symmetric])
- unfolding minus_minus
- apply (rule integrable_integral)
- apply (rule integrable_subinterval_real,rule integrable_continuous_real)
- apply (rule assms)+
- proof -
- show "{y .. x} \<subseteq> {a .. b}"
- using prems assms(2) by auto
- have *: "x - y = norm (y - x)"
- using True by auto
- show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y .. x}"
- apply (subst *)
- unfolding **
- apply blast
- done
- show "\<forall>xa\<in>{y .. x}. norm (f xa - f x) \<le> e"
- apply safe
- apply (rule less_imp_le)
- apply (rule d(2)[unfolded dist_norm])
- using assms(2)
- using prems
- apply auto
- done
- qed (insert e, auto)
- qed
- qed
-qed
+apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real])
+using assms
+apply (auto simp: continuous_on_eq_continuous_within)
+done
lemma antiderivative_continuous:
fixes q b :: real
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Sep 21 19:52:13 2015 +0100
@@ -437,11 +437,8 @@
apply (auto simp: continuous_on_op_minus)
done
-lemma forall_01_trivial: "(\<forall>x\<in>{0..1}. x \<le> 0 \<longrightarrow> P x) \<longleftrightarrow> P (0::real)"
- by auto
-
-lemma forall_half1_trivial: "(\<forall>x\<in>{1/2..1}. x * 2 \<le> 1 \<longrightarrow> P x) \<longleftrightarrow> P (1/2::real)"
- by auto (metis add_divide_distrib mult_2_right real_sum_of_halves)
+lemma half_bounded_equal: "1 \<le> x * 2 \<Longrightarrow> x * 2 \<le> 1 \<longleftrightarrow> x = (1/2::real)"
+ by simp
lemma continuous_on_joinpaths:
assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2"
@@ -451,17 +448,17 @@
by auto
have gg: "g2 0 = g1 1"
by (metis assms(3) pathfinish_def pathstart_def)
- have 1: "continuous_on {0..1 / 2} (g1 +++ g2)"
+ have 1: "continuous_on {0..1/2} (g1 +++ g2)"
apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"])
- apply (simp add: joinpaths_def)
- apply (rule continuous_intros | simp add: assms)+
+ apply (rule continuous_intros | simp add: joinpaths_def assms)+
done
- have 2: "continuous_on {1 / 2..1} (g1 +++ g2)"
- apply (rule continuous_on_eq [of _ "g2 o (\<lambda>x. 2*x-1)"])
- apply (simp add: joinpaths_def)
- apply (rule continuous_intros | simp add: forall_half1_trivial gg)+
- apply (rule continuous_on_subset)
- apply (rule assms, auto)
+ have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x-1))"
+ apply (rule continuous_on_subset [of "{1/2..1}"])
+ apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+
+ done
+ then have 2: "continuous_on {1/2..1} (g1 +++ g2)"
+ apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x-1)"])
+ apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+
done
show ?thesis
apply (subst *)
@@ -800,7 +797,6 @@
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"])
prefer 3
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a - 1 + x)"])
- defer
prefer 3
apply (rule continuous_intros)+
prefer 2
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 21 19:52:13 2015 +0100
@@ -2309,13 +2309,7 @@
subsection \<open>More properties of closed balls\<close>
-lemma closed_vimage: (* TODO: move to Topological_Spaces.thy *)
- assumes "closed s" and "continuous_on UNIV f"
- shows "closed (vimage f s)"
- using assms unfolding continuous_on_closed_vimage [OF closed_UNIV]
- by simp
-
-lemma closed_cball: "closed (cball x e)"
+lemma closed_cball [iff]: "closed (cball x e)"
proof -
have "closed (dist x -` {..e})"
by (intro closed_vimage closed_atMost continuous_intros)
@@ -4663,7 +4657,7 @@
by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
lemma continuous_on_eq:
- "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
+ "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
unfolding continuous_on_def tendsto_def eventually_at_topological
by simp
--- a/src/HOL/Real.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Real.thy Mon Sep 21 19:52:13 2015 +0100
@@ -22,6 +22,13 @@
subsection \<open>Preliminary lemmas\<close>
+lemma inj_add_left [simp]:
+ fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
+by (meson add_left_imp_eq injI)
+
+lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)"
+ by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
+
lemma add_diff_add:
fixes a b c d :: "'a::ab_group_add"
shows "(a + c) - (b + d) = (a - b) + (c - d)"
--- a/src/HOL/Set_Interval.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 21 19:52:13 2015 +0100
@@ -863,6 +863,14 @@
using image_affinity_atLeastAtMost [of m "-c" a b]
by simp
+lemma image_affinity_atLeastAtMost_div:
+ fixes c :: "'a::linordered_field"
+ shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {a/m + c .. b/m + c}
+ else {b/m + c .. a/m + c})"
+ using image_affinity_atLeastAtMost [of "inverse m" c a b]
+ by (simp add: field_class.field_divide_inverse algebra_simps)
+
lemma image_affinity_atLeastAtMost_div_diff:
fixes c :: "'a::linordered_field"
shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
--- a/src/HOL/Topological_Spaces.thy Mon Sep 21 14:44:32 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Sep 21 19:52:13 2015 +0100
@@ -1392,6 +1392,10 @@
"(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+lemma continuous_on_open_Un:
+ "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+ using continuous_on_open_Union [of "{s,t}"] by auto
+
lemma continuous_on_closed_Un:
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)