diff -r c095d3143047 -r dca11678c495 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Limits.thy	Wed May 13 12:55:33 2020 +0200
@@ -1227,6 +1227,33 @@
   shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   using assms unfolding continuous_on_def by (blast intro: tendsto_divide)
 
+lemma tendsto_power_int [tendsto_intros]:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes f: "(f \<longlongrightarrow> a) F"
+    and a: "a \<noteq> 0"
+  shows "((\<lambda>x. power_int (f x) n) \<longlongrightarrow> power_int a n) F"
+  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)
+
+lemma continuous_power_int:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous F f"
+    and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
+  shows "continuous F (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_def by (rule tendsto_power_int)
+
+lemma continuous_at_within_power_int[continuous_intros]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous (at a within s) f"
+    and "f a \<noteq> 0"
+  shows "continuous (at a within s) (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_within by (rule tendsto_power_int)
+
+lemma continuous_on_power_int [continuous_intros]:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+  shows "continuous_on s (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_on_def by (blast intro: tendsto_power_int)
+
 lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F"
   for l :: "'a::real_normed_vector"
   unfolding sgn_div_norm by (simp add: tendsto_intros)