Theorems · Theorem · field theory
inv_nhdsGT_zero
∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
[OrderTopology 𝕜], (nhdsWithin 0 (Set.Ioi 0))⁻¹ = Filter.atTop- Defined in
- Mathlib.Topology.Algebra.Order.Field
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Filterstatement and proof · cited by 8,121
- IsStrictOrderedRingstatement and proof · cited by 2,490
- Filter.atTopstatement and proof · cited by 2,405
- nhdsWithinstatement · cited by 1,912
- Set.Ioistatement · cited by 1,463
- OrderTopologystatement and proof · cited by 1,355
- inv_invproof · cited by 494
- Semifieldstatement and proof · cited by 439
- inv_atTop₀proof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- tendsto_inv_nhdsGT_zeroproof · cited by 9
- mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTopproof · cited by 0