equal
deleted
inserted
replaced
3594 "((ereal \<circ> f) \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)" |
3594 "((ereal \<circ> f) \<longlongrightarrow> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)" |
3595 "((ereal \<circ> f) \<longlongrightarrow> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)" |
3595 "((ereal \<circ> f) \<longlongrightarrow> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)" |
3596 unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense |
3596 unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense |
3597 using lim_ereal by (simp_all add: comp_def) |
3597 using lim_ereal by (simp_all add: comp_def) |
3598 |
3598 |
3599 lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)" |
3599 lemma inverse_infty_ereal_tendsto_0: "inverse \<midarrow>\<infinity>\<rightarrow> (0::ereal)" |
3600 proof - |
3600 proof - |
3601 have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity" |
3601 have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity" |
3602 by (intro tendsto_intros tendsto_inverse_0) |
3602 by (intro tendsto_intros tendsto_inverse_0) |
3603 |
3603 |
3604 show ?thesis |
3604 show ?thesis |
3607 intro!: filterlim_mono_eventually[OF **]) |
3607 intro!: filterlim_mono_eventually[OF **]) |
3608 qed |
3608 qed |
3609 |
3609 |
3610 lemma inverse_ereal_tendsto_pos: |
3610 lemma inverse_ereal_tendsto_pos: |
3611 fixes x :: ereal assumes "0 < x" |
3611 fixes x :: ereal assumes "0 < x" |
3612 shows "inverse -- x --> inverse x" |
3612 shows "inverse \<midarrow>x\<rightarrow> inverse x" |
3613 proof (cases x) |
3613 proof (cases x) |
3614 case (real r) |
3614 case (real r) |
3615 with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)" |
3615 with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) \<midarrow>r\<rightarrow> ereal (inverse r)" |
3616 by (auto intro!: tendsto_inverse) |
3616 by (auto intro!: tendsto_inverse) |
3617 from real \<open>0 < x\<close> show ?thesis |
3617 from real \<open>0 < x\<close> show ?thesis |
3618 by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter |
3618 by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter |
3619 intro!: Lim_transform_eventually[OF _ **] t1_space_nhds) |
3619 intro!: Lim_transform_eventually[OF _ **] t1_space_nhds) |
3620 qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0) |
3620 qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0) |