Theorems · Theorem · general topology
EReal.tendsto_nhds_top_iff_real
∀ {α : Type u_2} {m : α → EReal} {f : Filter α}, Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a- Defined in
- Mathlib.Topology.Instances.EReal.Lemmas
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Top.topstatement · cited by 9,680
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.Eventuallystatement and proof · cited by 3,134
- ERealstatement and proof · cited by 793
- Real.toERealstatement and proof · cited by 303
- Filter.HasBasis.tendsto_right_iffproof · cited by 81
- EReal.nhds_top_basisproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_posproof · cited by 3
- LinearGrowth.tendsto_atTop_of_linearGrowthInf_posproof · cited by 1
- EReal.tendsto_coe_nhds_top_iffproof · cited by 1