--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun Aug 25 22:17:24 2019 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Aug 27 17:08:51 2019 +0200
@@ -1247,15 +1247,6 @@
done
qed
-lemma has_derivative_componentwise_within:
- "(f has_derivative f') (at a within S) \<longleftrightarrow>
- (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
- apply (simp add: has_derivative_within)
- apply (subst tendsto_componentwise_iff)
- apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib)
- apply (simp add: algebra_simps)
- done
-
lemma differentiable_componentwise_within:
"f differentiable (at a within S) \<longleftrightarrow>
(\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)"