Theorems · Definition · logic and foundations
Hyperreal.Infinite
Deprecated since 2026-01-05Use ArchimedeanClass.mk instead.
ℝ* → Prop
A hyperreal number is infinite if it is infinite positive or infinite negative.
Do not use. Write ArchimedeanClass.mk x < 0 instead.
- Defined in
- Mathlib.Analysis.Real.Hyperreal
- Cited by
- 45 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Hyperrealstatement and proof · cited by 172
- Hyperreal.InfinitePosproof · cited by 44
- Hyperreal.InfiniteNegproof · cited by 38
Cited by45
Results whose statement or proof uses this declaration.
- Hyperreal.isSt_st'statement and proof · cited by 7
- Hyperreal.exists_st_of_not_infinitestatement and proof · cited by 4
- Hyperreal.IsSt.not_infinitestatement and proof · cited by 4
- Hyperreal.Infinite.not_infinitesimalstatement and proof · cited by 3
- Hyperreal.Infinite.st_eqstatement and proof · cited by 2
- Hyperreal.infinitePos_iff_infinite_of_nonnegstatement · cited by 2
- Hyperreal.infinite_iff_infinitesimal_invstatement · cited by 2
- Hyperreal.infinite_mul_of_infinite_not_infinitesimalstatement and proof · cited by 2
- Hyperreal.infinite_negstatement · cited by 2
- Hyperreal.isSt_sSupstatement and proof · cited by 2
- Hyperreal.not_infinite_of_exists_ststatement and proof · cited by 2
- Hyperreal.Infinite.ne_zerostatement and proof · cited by 1