Construction of the hyperreal numbers as an ultraproduct of real sequences

We define the Hyperreal numbers as quotients of sequences ℕ → ℝ by an ultrafilter. These form a field, and we prove some of their basic properties.

Note that most of the machinery that is usually defined for the specific purpose of non-standard analysis (infinitesimal and infinite elements, standard parts) has been generalized to other non-archimedean fields. In particular:

• ArchimedeanClass can be used to measure whether an element is infinitesimal (0 < mk x) or infinite (mk x < 0).
• ArchimedeanClass.stdPart generalizes the standard part function to a general ordered field.

Todo

Use Łoś's Theorem FirstOrder.Language.Ultraproduct.sentence_realize to formalize the transfer principle on Hyperreal.

def Hyperreal : Type

Hyperreal numbers on the ultrafilter extending the cofinite filter.

Equations

• ℝ* = (↑(Filter.hyperfilter ℕ)).Germ ℝ

def Hyperreal.«termℝ*» : Lean.ParserDescr

Hyperreal numbers on the ultrafilter extending the cofinite filter.

Equations

• Hyperreal.«termℝ*» = Lean.ParserDescr.node `Hyperreal.«termℝ*» 1024 (Lean.ParserDescr.symbol "ℝ*")

@[implicit_reducible]

noncomputable instance Hyperreal.instField : Field ℝ*

Equations

• Hyperreal.instField = inferInstanceAs (Field ((↑(Filter.hyperfilter ℕ)).Germ ℝ))

@[implicit_reducible]

noncomputable instance Hyperreal.instLinearOrder : LinearOrder ℝ*

Equations

• Hyperreal.instLinearOrder = inferInstanceAs (LinearOrder ((↑(Filter.hyperfilter ℕ)).Germ ℝ))

instance Hyperreal.instIsStrictOrderedRing : IsStrictOrderedRing ℝ*

noncomputable def Hyperreal.ofReal : ℝ → ℝ*

Natural embedding ℝ → ℝ*.

Equations

• Hyperreal.ofReal = Filter.Germ.const

@[implicit_reducible]

noncomputable instance Hyperreal.instCoeTCReal : CoeTC ℝ ℝ*

Equations

• Hyperreal.instCoeTCReal = { coe := Hyperreal.ofReal }

@[simp]

theorem Hyperreal.coe_eq_coe {x y : ℝ} : ↑x = ↑y ↔ x = y

theorem Hyperreal.coe_ne_coe {x y : ℝ} : ↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem Hyperreal.coe_eq_zero {x : ℝ} : ↑x = 0 ↔ x = 0

@[simp]

theorem Hyperreal.coe_eq_one {x : ℝ} : ↑x = 1 ↔ x = 1

theorem Hyperreal.coe_ne_zero {x : ℝ} : ↑x ≠ 0 ↔ x ≠ 0

theorem Hyperreal.coe_ne_one {x : ℝ} : ↑x ≠ 1 ↔ x ≠ 1

@[simp]

theorem Hyperreal.coe_one : ↑1 = 1

@[simp]

theorem Hyperreal.coe_zero : ↑0 = 0

@[simp]

theorem Hyperreal.coe_inv (x : ℝ) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem Hyperreal.coe_neg (x : ℝ) : ↑(-x) = -↑x

@[simp]

theorem Hyperreal.coe_add (x y : ℝ) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Hyperreal.coe_ofNat (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Hyperreal.coe_mul (x y : ℝ) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Hyperreal.coe_div (x y : ℝ) : ↑(x / y) = ↑x / ↑y

@[simp]

theorem Hyperreal.coe_sub (x y : ℝ) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Hyperreal.coe_le_coe {x y : ℝ} : ↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Hyperreal.coe_lt_coe {x y : ℝ} : ↑x < ↑y ↔ x < y

@[simp]

theorem Hyperreal.coe_nonneg {x : ℝ} : 0 ≤ ↑x ↔ 0 ≤ x

@[simp]

theorem Hyperreal.coe_pos {x : ℝ} : 0 < ↑x ↔ 0 < x

@[simp]

theorem Hyperreal.coe_abs (x : ℝ) : ↑|x| = |↑x|

@[simp]

theorem Hyperreal.coe_max (x y : ℝ) : ↑(max x y) = max ↑x ↑y

@[simp]

theorem Hyperreal.coe_min (x y : ℝ) : ↑(min x y) = min ↑x ↑y

noncomputable def Hyperreal.coeRingHom : ℝ →+*o ℝ*

The canonical map ℝ → ℝ* as an OrderRingHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hyperreal.coeRingHom_toFun (x : ℝ) : coeRingHom x = ↑x

@[simp]

theorem Hyperreal.archimedeanClassMk_coe_nonneg (x : ℝ) : 0 ≤ ArchimedeanClass.mk ↑x

@[simp]

theorem Hyperreal.archimdeanClassMk_coe {x : ℝ} (hx : x ≠ 0) : ArchimedeanClass.mk ↑x = 0

@[simp]

theorem Hyperreal.stdPart_coe (x : ℝ) : ArchimedeanClass.stdPart ↑x = x

Basic constants

noncomputable def Hyperreal.ofSeq (f : ℕ → ℝ) : ℝ*

Construct a hyperreal number from a sequence of real numbers.

Equations

• Hyperreal.ofSeq f = ↑f

theorem Hyperreal.ofSeq_surjective : Function.Surjective ofSeq

theorem Hyperreal.ofSeq_lt_ofSeq {f g : ℕ → ℝ} : ofSeq f < ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n < g n

theorem Hyperreal.ofSeq_le_ofSeq {f g : ℕ → ℝ} : ofSeq f ≤ ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n ≤ g n

ω

noncomputable def Hyperreal.omega : ℝ*

A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega.

Equations

• Hyperreal.omega = Hyperreal.ofSeq Nat.cast

def Hyperreal.termω : Lean.ParserDescr

A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ω in identifiers is omega.

Equations

• Hyperreal.termω = Lean.ParserDescr.node `Hyperreal.termω 1024 (Lean.ParserDescr.symbol "ω")

theorem Hyperreal.coe_lt_omega (r : ℝ) : ↑r < omega

theorem Hyperreal.omega_pos : 0 < omega

@[simp]

theorem Hyperreal.omega_ne_zero : omega ≠ 0

@[simp]

theorem Hyperreal.abs_omega : |omega| = omega

@[simp]

theorem Hyperreal.archimedeanClassMk_omega_neg : ArchimedeanClass.mk omega < 0

@[simp]

theorem Hyperreal.stdPart_omega : ArchimedeanClass.stdPart omega = 0

ε

noncomputable def Hyperreal.epsilon : ℝ*

A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ε in identifiers is epsilon.

Equations

• Hyperreal.epsilon = Hyperreal.ofSeq fun (n : ℕ) => (↑n)⁻¹

def Hyperreal.termε : Lean.ParserDescr

A sample infinitesimal hyperreal ε = ⟦(0, 1, 1/2, 1/3, ⋯)⟧.

Conventions for notations in identifiers:

• The recommended spelling of ε in identifiers is epsilon.

Equations

• Hyperreal.termε = Lean.ParserDescr.node `Hyperreal.termε 1024 (Lean.ParserDescr.symbol "ε")

@[simp]

theorem Hyperreal.inv_omega : omega⁻¹ = epsilon

@[simp]

theorem Hyperreal.inv_epsilon : epsilon⁻¹ = omega

@[simp]

theorem Hyperreal.epsilon_pos : 0 < epsilon

@[simp]

theorem Hyperreal.epsilon_ne_zero : epsilon ≠ 0

@[simp]

theorem Hyperreal.epsilon_mul_omega : epsilon * omega = 1

@[simp]

theorem Hyperreal.archimedeanClassMk_epsilon_pos : 0 < ArchimedeanClass.mk epsilon

Some facts about Tendsto

@[simp]

theorem Hyperreal.tendsto_ofSeq {f : ℕ → ℝ} {lb : Filter ℝ} : Filter.Germ.Tendsto (ofSeq f) lb ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) lb

theorem Hyperreal.stdPart_map {x : ℝ*} {r : ℝ} {f : ℝ → ℝ} (hf : ContinuousAt f r) (hxr : Filter.Germ.Tendsto x (nhds r)) : (Filter.Germ.map f x).Tendsto (nhds (f r))

theorem Hyperreal.stdPart_map₂ {x y : ℝ*} {r s : ℝ} {f : ℝ → ℝ → ℝ} (hxr : Filter.Germ.Tendsto x (nhds r)) (hys : Filter.Germ.Tendsto y (nhds s)) (hf : ContinuousAt (Function.uncurry f) (r, s)) : (Filter.Germ.map₂ f x y).Tendsto (nhds (f r s))

theorem Hyperreal.tendsto_iff_forall {x : ℝ*} {r : ℝ} : Filter.Germ.Tendsto x (nhds r) ↔ (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s

theorem Hyperreal.archimedeanClassMk_nonneg_of_tendsto {x : ℝ*} {r : ℝ} (hx : Filter.Germ.Tendsto x (nhds r)) : 0 ≤ ArchimedeanClass.mk x

theorem Hyperreal.stdPart_of_tendsto {x : ℝ*} {r : ℝ} (hx : Filter.Germ.Tendsto x (nhds r)) : ArchimedeanClass.stdPart x = r

theorem Hyperreal.archimedeanClassMk_pos_of_tendsto {x : ℝ*} (hx : Filter.Germ.Tendsto x (nhds 0)) : 0 < ArchimedeanClass.mk x

@[simp]

theorem Hyperreal.stdPart_epsilon : ArchimedeanClass.stdPart epsilon = 0

theorem Hyperreal.epsilon_lt_of_pos {r : ℝ} : 0 < r → epsilon < ↑r

theorem Hyperreal.epsilon_lt_of_neg {r : ℝ} : r < 0 → ↑r < epsilon

@[deprecated Hyperreal.epsilon_lt_of_pos (since := "2026-01-05")]

theorem Hyperreal.epsilon_lt_pos {r : ℝ} : 0 < r → epsilon < ↑r

Alias of Hyperreal.epsilon_lt_of_pos.

@[deprecated Hyperreal.archimedeanClassMk_pos_of_tendsto (since := "2026-01-05")]

theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : 0 < r → ofSeq f < ↑r

@[deprecated Hyperreal.archimedeanClassMk_pos_of_tendsto (since := "2026-01-05")]

theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : 0 < r → -↑r < ofSeq f

@[deprecated Hyperreal.archimedeanClassMk_pos_of_tendsto (since := "2026-01-05")]

theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : ℝ} : r < 0 → ↑r < ofSeq f

theorem Hyperreal.lt_of_tendsto_atTop {x : ℝ*} (r : ℝ) (hx : Filter.Germ.Tendsto x Filter.atTop) : ↑r < x

theorem Hyperreal.lt_of_tendsto_atBot {x : ℝ*} (r : ℝ) (hx : Filter.Germ.Tendsto x Filter.atBot) : x < ↑r

theorem Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop {x : ℝ*} (hx : Filter.Germ.Tendsto x Filter.atTop) : ArchimedeanClass.mk x < 0

theorem Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot {x : ℝ*} (hx : Filter.Germ.Tendsto x Filter.atBot) : ArchimedeanClass.mk x < 0

theorem Hyperreal.tendsto_atTop_iff {x : ℝ*} : Filter.Germ.Tendsto x Filter.atTop ↔ 0 < x ∧ ArchimedeanClass.mk x < 0

theorem Hyperreal.tendsto_atBot_iff {x : ℝ*} : Filter.Germ.Tendsto x Filter.atBot ↔ x < 0 ∧ ArchimedeanClass.mk x < 0

@[deprecated ArchimedeanClass.stdPart (since := "2026-01-05")]

def Hyperreal.IsSt (x : ℝ*) (r : ℝ) : Prop

Standard part predicate. Do not use. This is equivalent to the conjunction of 0 ≤ ArchimedeanClass.mk x and ArchimedeanClass.stdPart x = r.

Equations

• x.IsSt r = ∀ (δ : ℝ), 0 < δ → ↑r - ↑δ < x ∧ x < ↑r + ↑δ

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_iff {x : ℝ*} {r : ℝ} : x.IsSt r ↔ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.stdPart x = r

@[deprecated ArchimedeanClass.stdPart (since := "2026-01-05")]

noncomputable def Hyperreal.st : ℝ* → ℝ

Standard part function: like a "round" to ℝ instead of ℤ

Equations

• x.st = if h : ∃ (r : ℝ), x.IsSt r then Classical.choose h else 0

@[deprecated "`st` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.st_eq (x : ℝ*) : x.st = ArchimedeanClass.stdPart x

@[deprecated ArchimedeanClass.mk (since := "2026-01-05")]

def Hyperreal.Infinitesimal (x : ℝ*) : Prop

A hyperreal number is infinitesimal if its standard part is 0. Do not use. Write 0 < ArchimedeanClass.mk x instead.

Equations

• x.Infinitesimal = x.IsSt 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_iff {x : ℝ*} : x.Infinitesimal ↔ 0 < ArchimedeanClass.mk x

@[deprecated ArchimedeanClass.mk (since := "2026-01-05")]

def Hyperreal.InfinitePos (x : ℝ*) : Prop

A hyperreal number is positive infinite if it is larger than all real numbers. Do not use. Write 0 < x ∧ ArchimedeanClass.mk x < 0 instead.

Equations

• x.InfinitePos = ∀ (r : ℝ), ↑r < x

@[deprecated "`InfinitePos` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_iff {x : ℝ*} : x.InfinitePos ↔ 0 < x ∧ ArchimedeanClass.mk x < 0

@[deprecated ArchimedeanClass.mk (since := "2026-01-05")]

def Hyperreal.InfiniteNeg (x : ℝ*) : Prop

A hyperreal number is negative infinite if it is smaller than all real numbers. Do not use. Write x < 0 ∧ ArchimedeanClass.mk x < 0 instead.

Equations

• x.InfiniteNeg = ∀ (r : ℝ), x < ↑r

@[deprecated "`InfiniteNeg` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_iff {x : ℝ*} : x.InfiniteNeg ↔ x < 0 ∧ ArchimedeanClass.mk x < 0

@[deprecated ArchimedeanClass.mk (since := "2026-01-05")]

def Hyperreal.Infinite (x : ℝ*) : Prop

A hyperreal number is infinite if it is infinite positive or infinite negative. Do not use. Write ArchimedeanClass.mk x < 0 instead.

Equations

• x.Infinite = (x.InfinitePos ∨ x.InfiniteNeg)

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_iff {x : ℝ*} : x.Infinite ↔ ArchimedeanClass.mk x < 0

@[deprecated Hyperreal.tendsto_iff_forall (since := "2026-01-05")]

theorem Hyperreal.isSt_ofSeq_iff_tendsto {f : ℕ → ℝ} {r : ℝ} : (ofSeq f).IsSt r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)

@[deprecated Hyperreal.tendsto_iff_forall (since := "2026-01-05")]

theorem Hyperreal.isSt_iff_tendsto {x : ℝ*} {r : ℝ} : x.IsSt r ↔ Filter.Germ.Tendsto x (nhds r)

@[deprecated Hyperreal.stdPart_of_tendsto (since := "2026-01-05")]

theorem Hyperreal.isSt_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : Filter.Tendsto f Filter.atTop (nhds r)) : (ofSeq f).IsSt r

@[deprecated "Use `stdPart_monotoneOn` and `MonotoneOn.reflect_lt`" (since := "2026-01-05")]

theorem Hyperreal.IsSt.lt {x y : ℝ*} {r s : ℝ} (hxr : x.IsSt r) (hys : y.IsSt s) (hrs : r < s) : x < y

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.IsSt.unique {x : ℝ*} {r s : ℝ} (hr : x.IsSt r) (hs : x.IsSt s) : r = s

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.IsSt.st_eq {x : ℝ*} {r : ℝ} (hxr : x.IsSt r) : x.st = r

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.IsSt.not_infinite {x : ℝ*} {r : ℝ} (h : x.IsSt r) : ¬x.Infinite

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_of_exists_st {x : ℝ*} : (∃ (r : ℝ), x.IsSt r) → ¬x.Infinite

@[deprecated ArchimedeanClass.stdPart_eq_zero (since := "2026-01-05")]

theorem Hyperreal.Infinite.st_eq {x : ℝ*} (hi : x.Infinite) : x.st = 0

@[deprecated ArchimedeanClass.stdPart_eq_sSup (since := "2026-01-05")]

theorem Hyperreal.isSt_sSup {x : ℝ*} (hni : ¬x.Infinite) : x.IsSt (sSup {y : ℝ | ↑y < x})

@[deprecated ArchimedeanClass.stdPart_eq_sSup (since := "2026-01-05")]

theorem Hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬x.Infinite) : ∃ (r : ℝ), x.IsSt r

@[deprecated ArchimedeanClass.stdPart_eq_sSup (since := "2026-01-05")]

theorem Hyperreal.st_eq_sSup {x : ℝ*} : x.st = sSup {y : ℝ | ↑y < x}

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.exists_st_iff_not_infinite {x : ℝ*} : (∃ (r : ℝ), x.IsSt r) ↔ ¬x.Infinite

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_iff_not_exists_st {x : ℝ*} : x.Infinite ↔ ¬∃ (r : ℝ), x.IsSt r

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.IsSt.isSt_st {x : ℝ*} {r : ℝ} (hxr : x.IsSt r) : x.IsSt x.st

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ℝ), x.IsSt r) : x.IsSt x.st

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_st' {x : ℝ*} (hx : ¬x.Infinite) : x.IsSt x.st

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_st {x : ℝ*} (hx : x.st ≠ 0) : x.IsSt x.st

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_refl_real (r : ℝ) : (↑r).IsSt r

@[deprecated Hyperreal.stdPart_coe (since := "2026-01-05")]

theorem Hyperreal.st_id_real (r : ℝ) : (↑r).st = r

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.eq_of_isSt_real {r s : ℝ} : (↑r).IsSt s → r = s

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_real_iff_eq {r s : ℝ} : (↑r).IsSt s ↔ r = s

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_symm_real {r s : ℝ} : (↑r).IsSt s ↔ (↑s).IsSt r

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_trans_real {r s t : ℝ} : (↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_inj_real {r₁ r₂ s : ℝ} (h1 : (↑r₁).IsSt s) (h2 : (↑r₂).IsSt s) : r₁ = r₂

@[deprecated "`IsSt` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} : x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ

@[deprecated Hyperreal.stdPart_map (since := "2026-01-05")]

theorem Hyperreal.IsSt.map {x : ℝ*} {r : ℝ} (hxr : x.IsSt r) {f : ℝ → ℝ} (hf : ContinuousAt f r) : IsSt (Filter.Germ.map f x) (f r)

@[deprecated Hyperreal.stdPart_map₂ (since := "2026-01-05")]

theorem Hyperreal.IsSt.map₂ {x y : ℝ*} {r s : ℝ} (hxr : x.IsSt r) (hys : y.IsSt s) {f : ℝ → ℝ → ℝ} (hf : ContinuousAt (Function.uncurry f) (r, s)) : IsSt (Filter.Germ.map₂ f x y) (f r s)

@[deprecated ArchimedeanClass.stdPart_add (since := "2026-01-05")]

theorem Hyperreal.IsSt.add {x y : ℝ*} {r s : ℝ} (hxr : x.IsSt r) (hys : y.IsSt s) : (x + y).IsSt (r + s)

@[deprecated ArchimedeanClass.stdPart_neg (since := "2026-01-05")]

theorem Hyperreal.IsSt.neg {x : ℝ*} {r : ℝ} (hxr : x.IsSt r) : (-x).IsSt (-r)

@[deprecated ArchimedeanClass.stdPart_sub (since := "2026-01-05")]

theorem Hyperreal.IsSt.sub {x y : ℝ*} {r s : ℝ} (hxr : x.IsSt r) (hys : y.IsSt s) : (x - y).IsSt (r - s)

@[deprecated ArchimedeanClass.stdPart_monotoneOn (since := "2026-01-05")]

theorem Hyperreal.IsSt.le {x y : ℝ*} {r s : ℝ} (hrx : x.IsSt r) (hsy : y.IsSt s) (hxy : x ≤ y) : r ≤ s

@[deprecated ArchimedeanClass.stdPart_monotoneOn (since := "2026-01-05")]

theorem Hyperreal.st_le_of_le {x y : ℝ*} (hix : ¬x.Infinite) (hiy : ¬y.Infinite) : x ≤ y → x.st ≤ y.st

@[deprecated ArchimedeanClass.stdPart_monotoneOn (since := "2026-01-05")]

theorem Hyperreal.lt_of_st_lt {x y : ℝ*} (hix : ¬x.Infinite) (hiy : ¬y.Infinite) : x.st < y.st → x < y

@[deprecated "`InfinitePos` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_def {x : ℝ*} : x.InfinitePos ↔ ∀ (r : ℝ), ↑r < x

@[deprecated "`InfiniteNeg` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_def {x : ℝ*} : x.InfiniteNeg ↔ ∀ (r : ℝ), x < ↑r

@[deprecated "`InfinitePos` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfinitePos.pos {x : ℝ*} (hip : x.InfinitePos) : 0 < x

@[deprecated "`InfiniteNeg` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfiniteNeg.lt_zero {x : ℝ*} : x.InfiniteNeg → x < 0

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinite.ne_zero {x : ℝ*} (hI : x.Infinite) : x ≠ 0

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_zero : ¬Infinite 0

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfiniteNeg.not_infinitePos {x : ℝ*} : x.InfiniteNeg → ¬x.InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfinitePos.not_infiniteNeg {x : ℝ*} (hp : x.InfinitePos) : ¬x.InfiniteNeg

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfinitePos.neg {x : ℝ*} : x.InfinitePos → (-x).InfiniteNeg

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfiniteNeg.neg {x : ℝ*} : x.InfiniteNeg → (-x).InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_neg {x : ℝ*} : (-x).InfiniteNeg ↔ x.InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_neg {x : ℝ*} : (-x).InfinitePos ↔ x.InfiniteNeg

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_neg {x : ℝ*} : (-x).Infinite ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinitesimal.not_infinite {x : ℝ*} (h : x.Infinitesimal) : ¬x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinite.not_infinitesimal {x : ℝ*} (h : x.Infinite) : ¬x.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfinitePos.not_infinitesimal {x : ℝ*} (h : x.InfinitePos) : ¬x.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.InfiniteNeg.not_infinitesimal {x : ℝ*} (h : x.InfiniteNeg) : ¬x.Infinitesimal

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_iff_infinite_and_pos {x : ℝ*} : x.InfinitePos ↔ x.Infinite ∧ 0 < x

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_iff_infinite_and_neg {x : ℝ*} : x.InfiniteNeg ↔ x.Infinite ∧ x < 0

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 ≤ x) : x.InfinitePos ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) : x.InfinitePos ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) : x.InfiniteNeg ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_abs_iff_infinite_abs {x : ℝ*} : |x|.InfinitePos ↔ |x|.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_abs_iff {x : ℝ*} : |x|.Infinite ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_abs_iff_infinite {x : ℝ*} : |x|.InfinitePos ↔ x.Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} : x.Infinite ↔ ∀ (r : ℝ), |↑r| < |x|

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_add_not_infiniteNeg {x y : ℝ*} : x.InfinitePos → ¬y.InfiniteNeg → (x + y).InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infiniteNeg_add_infinitePos {x y : ℝ*} : ¬x.InfiniteNeg → y.InfinitePos → (x + y).InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_add_not_infinitePos {x y : ℝ*} : x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinitePos_add_infiniteNeg {x y : ℝ*} : ¬x.InfinitePos → y.InfiniteNeg → (x + y).InfiniteNeg

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_add_infinitePos {x y : ℝ*} : x.InfinitePos → y.InfinitePos → (x + y).InfinitePos

@[deprecated "`InfinitePos` and `InfiniteNeg` are deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_add_infiniteNeg {x y : ℝ*} : x.InfiniteNeg → y.InfiniteNeg → (x + y).InfiniteNeg

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_add_not_infinite {x y : ℝ*} : x.InfinitePos → ¬y.Infinite → (x + y).InfinitePos

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_add_not_infinite {x y : ℝ*} : x.InfiniteNeg → ¬y.Infinite → (x + y).InfiniteNeg

@[deprecated "`InfinitePos` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_of_tendsto_top {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) : (ofSeq f).InfinitePos

@[deprecated "`InfiniteNeg` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_of_tendsto_bot {f : ℕ → ℝ} (hf : Filter.Tendsto f Filter.atTop Filter.atBot) : (ofSeq f).InfiniteNeg

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_neg {x : ℝ*} : ¬x.Infinite → ¬(-x).Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_add {x y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) : ¬(x + y).Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬x.Infinite ↔ ∃ (r : ℝ) (s : ℝ), ↑r < x ∧ x < ↑s

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_infinite_real (r : ℝ) : ¬(↑r).Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinite.ne_real {x : ℝ*} : x.Infinite → ∀ (r : ℝ), x ≠ ↑r

Facts about st that require some infinite machinery

@[deprecated ArchimedeanClass.stdPart_mul (since := "2026-01-05")]

theorem Hyperreal.IsSt.mul {x y : ℝ*} {r s : ℝ} (hxr : x.IsSt r) (hys : y.IsSt s) : (x * y).IsSt (r * s)

@[deprecated ArchimedeanClass.mk_mul (since := "2026-01-05")]

theorem Hyperreal.not_infinite_mul {x y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) : ¬(x * y).Infinite

@[deprecated ArchimedeanClass.stdPart_add (since := "2026-01-05")]

theorem Hyperreal.st_add {x y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) : (x + y).st = x.st + y.st

@[deprecated ArchimedeanClass.stdPart_neg (since := "2026-01-05")]

theorem Hyperreal.st_neg (x : ℝ*) : (-x).st = -x.st

@[deprecated ArchimedeanClass.stdPart_mul (since := "2026-01-05")]

theorem Hyperreal.st_mul {x y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) : (x * y).st = x.st * y.st

Basic lemmas about infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_def {x : ℝ*} : x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r

@[deprecated ArchimedeanClass.lt_of_pos_of_archimedean (since := "2026-01-05")]

theorem Hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} : x.Infinitesimal → ∀ (r : ℝ), 0 < r → x < ↑r

@[deprecated ArchimedeanClass.lt_of_neg_of_archimedean (since := "2026-01-05")]

theorem Hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} : x.Infinitesimal → ∀ (r : ℝ), 0 < r → -↑r < x

@[deprecated ArchimedeanClass.lt_of_neg_of_archimedean (since := "2026-01-05")]

theorem Hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (hi : x.Infinitesimal) (r : ℝ) (hr : r < 0) : ↑r < x

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} : x.Infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |↑r|

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_zero : Infinitesimal 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinitesimal.eq_zero {r : ℝ} : (↑r).Infinitesimal → r = 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_real_iff {r : ℝ} : (↑r).Infinitesimal ↔ r = 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinitesimal.add {x y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) : (x + y).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinitesimal.neg {x : ℝ*} (hx : x.Infinitesimal) : (-x).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_neg {x : ℝ*} : (-x).Infinitesimal ↔ x.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinitesimal.mul {x y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) : (x * y).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (h : Filter.Tendsto f Filter.atTop (nhds 0)) : (ofSeq f).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_epsilon : epsilon.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) : x.Infinitesimal → x ≠ 0 → ∀ (r : ℝ), x ≠ ↑r

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.IsSt.infinitesimal_sub {x : ℝ*} {r : ℝ} (hxr : x.IsSt r) : (x - ↑r).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_sub_st {x : ℝ*} (hx : ¬x.Infinite) : (x - ↑x.st).Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos {x : ℝ*} : x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} : x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_inv_of_infinite {x : ℝ*} : x.Infinite → x⁻¹.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : x⁻¹.Infinitesimal) : x.Infinite

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) : x.Infinite ↔ x⁻¹.Infinitesimal

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} : x⁻¹.InfinitePos ↔ x.Infinitesimal ∧ 0 < x

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} : x⁻¹.InfiniteNeg ↔ x.Infinitesimal ∧ x < 0

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : x.Infinitesimal ↔ x⁻¹.Infinite

@[deprecated ArchimedeanClass.stdPart_inv (since := "2026-01-05")]

theorem Hyperreal.IsSt.inv {x : ℝ*} {r : ℝ} (hi : ¬x.Infinitesimal) (hr : x.IsSt r) : x⁻¹.IsSt r⁻¹

@[deprecated ArchimedeanClass.stdPart_inv (since := "2026-01-05")]

theorem Hyperreal.st_inv (x : ℝ*) : x⁻¹.st = x.st⁻¹

@[deprecated Hyperreal.archimedeanClassMk_omega_neg (since := "2026-01-05")]

theorem Hyperreal.infinitePos_omega : omega.InfinitePos

@[deprecated Hyperreal.archimedeanClassMk_omega_neg (since := "2026-01-05")]

theorem Hyperreal.infinite_omega : omega.Infinite

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos {x y : ℝ*} : x.InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos {x y : ℝ*} : ¬x.Infinitesimal → 0 < x → y.InfinitePos → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg {x y : ℝ*} : x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg {x y : ℝ*} : ¬x.Infinitesimal → x < 0 → y.InfiniteNeg → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x y : ℝ*} : x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos {x y : ℝ*} : ¬x.Infinitesimal → x < 0 → y.InfinitePos → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x y : ℝ*} : x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x y : ℝ*} : ¬x.Infinitesimal → 0 < x → y.InfiniteNeg → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_infinitePos {x y : ℝ*} : x.InfinitePos → y.InfinitePos → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_infiniteNeg {x y : ℝ*} : x.InfiniteNeg → y.InfiniteNeg → (x * y).InfinitePos

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinitePos_mul_infiniteNeg {x y : ℝ*} : x.InfinitePos → y.InfiniteNeg → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infiniteNeg_mul_infinitePos {x y : ℝ*} : x.InfiniteNeg → y.InfinitePos → (x * y).InfiniteNeg

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} : x.Infinite → ¬y.Infinitesimal → (x * y).Infinite

@[deprecated "`Infinitesimal` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} : ¬x.Infinitesimal → y.Infinite → (x * y).Infinite

@[deprecated "`Infinite` is deprecated" (since := "2026-01-05")]

theorem Hyperreal.Infinite.mul {x y : ℝ*} : x.Infinite → y.Infinite → (x * y).Infinite