Construction of the hyperreal numbers as an ultraproduct of real sequences.

def Hyperreal : Type

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations

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

instance instHyperrealInhabited : Inhabited ℝ*

Equations

• instHyperrealInhabited = Filter.Germ.instInhabited

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 "ℝ*")

noncomputable instance Hyperreal.instLinearOrderedField : LinearOrderedField ℝ*

Equations

• Hyperreal.instLinearOrderedField = inferInstanceAs (LinearOrderedField ((↑(Filter.hyperfilter ℕ)).Germ ℝ))

def Hyperreal.ofReal : ℝ → ℝ*

Natural embedding ℝ → ℝ*.

Equations

• Hyperreal.ofReal = Filter.Germ.const

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

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 Hyperreal.ofSeq

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

noncomputable def Hyperreal.epsilon : ℝ*

A sample infinitesimal hyperreal

Equations

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

noncomputable def Hyperreal.omega : ℝ*

A sample infinite hyperreal

Equations

• Hyperreal.omega = Hyperreal.ofSeq Nat.cast

def Hyperreal.termε : Lean.ParserDescr

A sample infinitesimal hyperreal

Equations

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

def Hyperreal.termω : Lean.ParserDescr

A sample infinite hyperreal

Equations

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

@[simp]

theorem Hyperreal.inv_omega : Hyperreal.omega⁻¹ = Hyperreal.epsilon

@[simp]

theorem Hyperreal.inv_epsilon : Hyperreal.epsilon⁻¹ = Hyperreal.omega

theorem Hyperreal.omega_pos : 0 < Hyperreal.omega

theorem Hyperreal.epsilon_pos : 0 < Hyperreal.epsilon

theorem Hyperreal.epsilon_ne_zero : Hyperreal.epsilon ≠ 0

theorem Hyperreal.omega_ne_zero : Hyperreal.omega ≠ 0

theorem Hyperreal.epsilon_mul_omega : Hyperreal.epsilon * Hyperreal.omega = 1

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

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

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

theorem Hyperreal.epsilon_lt_pos (x : ℝ) : 0 < x → Hyperreal.epsilon < ↑x

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

Standard part predicate

Equations

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

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

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

A hyperreal number is infinitesimal if its standard part is 0

Equations

• x.Infinitesimal = x.IsSt 0

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

A hyperreal number is positive infinite if it is larger than all real numbers

Equations

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

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

A hyperreal number is negative infinite if it is smaller than all real numbers

Equations

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

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

A hyperreal number is infinite if it is infinite positive or infinite negative

Equations

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

Some facts about st

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Basic lemmas about infinite

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

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

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

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

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

theorem Hyperreal.not_infinite_zero : ¬Hyperreal.Infinite 0

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Facts about st that require some infinite machinery

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

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

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

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

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

Basic lemmas about infinitesimal

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

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

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

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

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

theorem Hyperreal.infinitesimal_zero : Hyperreal.Infinitesimal 0

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

@[simp]

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

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

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

@[simp]

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

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

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

theorem Hyperreal.infinitesimal_epsilon : Hyperreal.epsilon.Infinitesimal

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

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

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

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

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

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

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

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

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

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

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

Hyperreal.st stuff that requires infinitesimal machinery

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

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

Infinite stuff that requires infinitesimal machinery

theorem Hyperreal.infinitePos_omega : Hyperreal.omega.InfinitePos

theorem Hyperreal.infinite_omega : Hyperreal.omega.Infinite

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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