# HG changeset patch
# User hoelzl
# Date 1301500441 -7200
# Node ID a28e87ed996f690d93a1008f0092a674880ed130
# Parent  f88c7315d72d4f7eb2e95d135367311c34da7949
real multiplication is continuous

diff -r f88c7315d72d -r a28e87ed996f src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 30 17:53:56 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 30 17:54:01 2011 +0200
@@ -3829,7 +3829,8 @@
              ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
   unfolding continuous_def by (intro tendsto_intros)
 
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
+lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
+  continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
 
 lemma continuous_on_vmul:
   fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -3843,9 +3844,20 @@
              ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
   unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
 
-lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
-  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
-  continuous_on_mul continuous_on_vmul
+lemma continuous_on_mul_real:
+  fixes f :: "'a::metric_space \<Rightarrow> real"
+  fixes g :: "'a::metric_space \<Rightarrow> real"
+  shows "continuous_on s f \<Longrightarrow> continuous_on s g
+             ==> continuous_on s (\<lambda>x. f x * g x)"
+  using continuous_on_mul[of s f g] unfolding real_scaleR_def .
+
+lemmas continuous_on_intros = continuous_on_add continuous_on_const
+  continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
+  continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
+  uniformly_continuous_on_add uniformly_continuous_on_const
+  uniformly_continuous_on_id uniformly_continuous_on_compose
+  uniformly_continuous_on_cmul uniformly_continuous_on_neg
+  uniformly_continuous_on_sub
 
 text{* And so we have continuity of inverse.                                     *}