Theorems · Theorem · approximation theory
Asymptotics.isBigO_const_of_tendsto
∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
{f'' : α → E''} {l : Filter α} {y : E''}, Filter.Tendsto f'' l (nhds y) → ∀ {c : F''}, c ≠ 0 → f'' =O[l] fun _x => c- Defined in
- Mathlib.Analysis.Asymptotics.Lemmas
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NormedAddCommGroupstatement and proof · cited by 15,752
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Asymptotics.IsBigOstatement · cited by 506
- Filter.Tendsto.normproof · cited by 44
- Filter.Tendsto.isBoundedUnder_leproof · cited by 25
- Filter.IsBoundedUnder.isBigO_constproof · cited by 6
Cited by4
Results whose statement or proof uses this declaration.
- Complex.tendsto_mul_log_one_add_of_tendstoproof · cited by 3
- HurwitzZeta.differentiableAt_update_of_residueproof · cited by 2
- Complex.hasDerivAt_GammaIntegralproof · cited by 1
- AkraBazziRecurrence.isBigO_asympBoundproof · cited by 1