Theorems · Theorem · order theory
tendsto_natCast_atTop_atTop
∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop- Cited by
- 51 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- PartialOrderstatement and proof · cited by 6,410
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- IsOrderedRingstatement and proof · cited by 777
- Archimedeanstatement and proof · cited by 603
- Nat.mono_castproof · cited by 76
- exists_nat_geproof · cited by 20
- Monotone.tendsto_atTop_atTopproof · cited by 13
Cited by51
Results whose statement or proof uses this declaration.
- summable_pow_mul_jacobiTheta₂_term_boundproof · cited by 6
- Filter.Eventually.natCast_atTopproof · cited by 6
- PairReduction.exists_radius_leproof · cited by 4
- summable_jacobiTheta₂_term_iffproof · cited by 4
- Asymptotics.isLittleO_sum_range_of_tendsto_zeroproof · cited by 3
- Real.tendsto_eulerMascheroniSeq'proof · cited by 3
- LiouvilleWith.frequently_lt_rpow_negproof · cited by 3
- MeasureTheory.hausdorffMeasure_pi_realproof · cited by 3
- ZetaAsymptotics.termTSum_of_ltproof · cited by 2
- Real.tendsto_log_nat_add_one_sub_logproof · cited by 2
- Asymptotics.IsBigO.natCast_atTopproof · cited by 2
- Real.tendsto_one_add_div_pow_expproof · cited by 2