equal
deleted
inserted
replaced
2319 lemma tendsto_powr [tendsto_intros]: (*FIXME a mess, suggests a general rule about exceptions*) |
2319 lemma tendsto_powr [tendsto_intros]: (*FIXME a mess, suggests a general rule about exceptions*) |
2320 fixes a::real |
2320 fixes a::real |
2321 shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F" |
2321 shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F" |
2322 apply (simp add: powr_def) |
2322 apply (simp add: powr_def) |
2323 apply (simp add: tendsto_def) |
2323 apply (simp add: tendsto_def) |
2324 apply (simp add: Topological_Spaces.eventually_conj_iff ) |
2324 apply (simp add: eventually_conj_iff ) |
2325 apply safe |
2325 apply safe |
2326 apply (case_tac "0 \<in> S") |
2326 apply (case_tac "0 \<in> S") |
2327 apply (auto simp: ) |
2327 apply (auto simp: ) |
2328 apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T") |
2328 apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T") |
2329 apply clarify |
2329 apply clarify |