equal
deleted
inserted
replaced
629 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
629 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
630 shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" |
630 shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" |
631 unfolding continuous_def by (rule tendsto_diff) |
631 unfolding continuous_def by (rule tendsto_diff) |
632 |
632 |
633 lemma continuous_on_diff [continuous_intros]: |
633 lemma continuous_on_diff [continuous_intros]: |
634 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
634 fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector" |
635 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)" |
635 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)" |
636 unfolding continuous_on_def by (auto intro: tendsto_diff) |
636 unfolding continuous_on_def by (auto intro: tendsto_diff) |
637 |
637 |
638 lemma continuous_on_op_minus: "continuous_on (s::'a::real_normed_vector set) (op - x)" |
638 lemma continuous_on_op_minus: "continuous_on (s::'a::real_normed_vector set) (op - x)" |
639 by (rule continuous_intros | simp)+ |
639 by (rule continuous_intros | simp)+ |