Theorems · Theorem · logic and foundations
Hyperreal.tendsto_atTop_iff
∀ {x : ℝ*}, Filter.Germ.Tendsto x Filter.atTop ↔ 0 < x ∧ ArchimedeanClass.mk x < 0- Defined in
- Mathlib.Analysis.Real.Hyperreal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
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
- Filter.atTopstatement and proof · cited by 2,405
- LT.lt.leproof · cited by 2,189
- LT.lt.trans_leproof · cited by 678
- ArchimedeanClassstatement · cited by 247
- ArchimedeanClass.mkstatement and proof · cited by 174
- Ultrafilter.toFilterstatement · cited by 172
- Hyperrealstatement and proof · cited by 172
- Filter.hyperfilterstatement · cited by 30
- Filter.tendsto_atTopproof · cited by 24
- Hyperreal.ofSeqproof · cited by 24
- Filter.Germ.Tendstostatement and proof · cited by 18
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.