Theorems · Theorem · sequences and series
tendsto_one_div_add_atTop_nhds_zero_nat
∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜],
Filter.Tendsto (fun n => 1 / (↑n + 1)) Filter.atTop (nhds 0)- Defined in
- Mathlib.Analysis.SpecificLimits.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Nat.cast_oneproof · cited by 2,501
- Filter.atTopstatement and proof · cited by 2,405
- ContinuousSMulstatement and proof · cited by 1,016
- CharZerostatement and proof · cited by 932
- one_divproof · cited by 624
- Nat.cast_addproof · cited by 586
- NNRatstatement and proof · cited by 523
- DivisionSemiringstatement and proof · cited by 216
- Filter.tendsto_add_atTop_iff_natproof · cited by 23
Cited by4
Results whose statement or proof uses this declaration.
- blimsup_cthickening_mul_ae_eqproof · cited by 2
- exists_norm_eq_iInf_of_complete_convexproof · cited by 1
- MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendstoproof · cited by 1
- perfectlyNormalSpace_iff_forall_isClosed_preimage_zeroproof · cited by 0