Theorems · Theorem · approximation theory
Asymptotics.isEquivalent_iff_tendsto_one
∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
(∀ᶠ (x : α) in l, v x ≠ 0) → (Asymptotics.IsEquivalent l u v ↔ Filter.Tendsto (u / v) l (nhds 1))- Cited by
- 3 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallystatement and proof · cited by 3,134
- zero_addproof · cited by 2,366
- NormedFieldstatement and proof · cited by 1,084
- Filter.Eventually.monoproof · cited by 646
- sub_add_cancelproof · cited by 344
- tendsto_const_nhdsproof · cited by 330
- div_selfproof · cited by 237
- Filter.Tendsto.addproof · cited by 102
Cited by3
Results whose statement or proof uses this declaration.
- isEquivalent_descFactorialproof · cited by 1
- Asymptotics.IsEquivalent.logproof · cited by 0
- SimpleGraph.isEquivalent_extremalNumberproof · cited by 0