Theorems · Theorem · approximation theory
LinearGrowth.le_linearGrowthInf_iff
∀ {u : ℕ → EReal} {a : EReal}, a ≤ LinearGrowth.linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in Filter.atTop, b * ↑n ≤ u n- Cited by
- 3 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filter.Eventuallystatement and proof · cited by 3,134
- Filter.atTopstatement and proof · cited by 2,405
- Nat.cast_zeroproof · cited by 1,870
- ERealstatement and proof · cited by 793
- Filter.eventually_atTopproof · cited by 112
- Filter.isBounded_ge_of_botproof · cited by 55
- LinearGrowth.linearGrowthInfstatement · cited by 41
- Filter.isCobounded_ge_of_topproof · cited by 38
- Filter.eventually_congrproof · cited by 20
- EReal.natCast_ne_topproof · cited by 19
- EReal.le_div_iff_mul_leproof · cited by 6
- Filter.le_liminf_iff'proof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- Eventually.le_linearGrowthInfproof · cited by 2
- LinearGrowth.tendsto_atTop_of_linearGrowthInf_posproof · cited by 1
- LinearGrowth.eventually_mul_leproof · cited by 1