Theorems · Theorem · special functions
Real.tendsto_mul_exp_add_div_pow_atTop
∀ (b c : ℝ) (n : ℕ), 0 < b → Filter.Tendsto (fun x => (b * Real.exp x + c) / x ^ n) Filter.atTop Filter.atTop
The function (b * exp x + c) / (x ^ n) tends to +∞ at +∞, for any natural number
n and any real numbers b and c such that b is positive.
- Defined in
- Mathlib.Analysis.SpecialFunctions.Exp
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopstatement and proof · cited by 2,405
- eq_or_neproof · cited by 1,117
- pow_zeroproof · cited by 1,094
- Real.expstatement and proof · cited by 871
- div_oneproof · cited by 629
- tendsto_const_nhdsproof · cited by 330
- mul_div_assocproof · cited by 149
- add_divproof · cited by 89
- Filter.Tendsto.const_mul_atTopproof · cited by 30
- Filter.tendsto_pow_atTopproof · cited by 14
Cited by1
Results whose statement or proof uses this declaration.
- Real.tendsto_div_pow_mul_exp_add_atTopproof · cited by 3