Theorems · Theorem · field theory
tendsto_zpow_atTop_zero
∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
[OrderTopology 𝕜] {n : ℤ}, n < 0 → Filter.Tendsto (fun x => x ^ n) Filter.atTop (nhds 0)- Defined in
- Mathlib.Topology.Algebra.Order.Field
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- LinearOrderstatement and proof · cited by 8,572
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- IsStrictOrderedRingstatement and proof · cited by 2,490
- Filter.atTopstatement and proof · cited by 2,405
- LT.lt.ne'proof · cited by 1,417
- OrderTopologystatement and proof · cited by 1,355
- le_of_ltproof · cited by 1,175
- neg_negproof · cited by 960
- Semifieldstatement and proof · cited by 439
- Nat.cast_posproof · cited by 113
Cited by4
Results whose statement or proof uses this declaration.
- Polynomial.div_tendsto_atTop_zero_of_degree_ltproof · cited by 5
- Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zeroproof · cited by 2
- tendsto_pow_div_pow_atTop_zeroproof · cited by 1
- tendsto_const_mul_zpow_atTop_zeroproof · cited by 1