Theorems · Theorem · field theory

tendsto_inv_nhdsGT_zero

∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun x => x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The function x ↦ x⁻¹ tends to +∞ on the right of 0.

Defined in

Mathlib.Topology.Algebra.Order.Field

Cited by

9 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemifieldLinearOrderIsStrictOrderedRingTopologicalSpaceOrderTopology