Theorems · Theorem · real analysis
Subadditive.eventually_div_lt_of_div_lt
∀ {u : ℕ → ℝ}, Subadditive u → ∀ {L : ℝ} {n : ℕ}, n ≠ 0 → u n / ↑n < L → ∀ᶠ (p : ℕ) in Filter.atTop, u p / ↑p < L- Defined in
- Mathlib.Analysis.Subadditive
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
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
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- Filter.Eventuallystatement · cited by 3,134
- add_zeroproof · cited by 2,707
- Filter.atTopstatement and proof · cited by 2,405
- mul_commproof · cited by 2,262
- Filter.Eventually.monoproof · cited by 646
- Filter.Tendsto.compproof · cited by 560
- lt_of_le_of_ltproof · cited by 432
- tendsto_const_nhdsproof · cited by 330
- Nat.cast_nonneg'proof · cited by 245
Cited by1
Results whose statement or proof uses this declaration.
- Subadditive.tendsto_limproof · cited by 0