mathlib documentation

data.real.hyperreal

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

source
def hyperreal  :
Type

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
source
@[instance]
def hyperreal.discrete_linear_ordered_field  :
discrete_linear_ordered_field ℝ*

Equations
source
@[instance]
def hyperreal.inhabited  :
inhabited ℝ*

Equations
source
@[instance]
def hyperreal.has_coe_t  :
has_coe_t ℝ ℝ*

Equations
source
@[simp]
theorem hyperreal.coe_eq_coe {x y : ℝ} :
↑x = ↑y ↔ x = y

source
@[simp]
theorem hyperreal.coe_eq_zero {x : ℝ} :
↑x = 0 ↔ x = 0

source
@[simp]
theorem hyperreal.coe_eq_one {x : ℝ} :
↑x = 1 ↔ x = 1

source
@[simp]
theorem hyperreal.coe_one  :
↑1 = 1

source
@[simp]
theorem hyperreal.coe_zero  :
↑0 = 0

source
@[simp]
theorem hyperreal.coe_inv (x : ℝ) :
↑x⁻¹ = (↑x)⁻¹

source
@[simp]
theorem hyperreal.coe_neg (x : ℝ) :
↑-x = -↑x

source
@[simp]
theorem hyperreal.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y

source
@[simp]
theorem hyperreal.coe_bit0 (x : ℝ) :
↑(bit0 x) = bit0 ↑x

source
@[simp]
theorem hyperreal.coe_bit1 (x : ℝ) :
↑(bit1 x) = bit1 ↑x

source
@[simp]
theorem hyperreal.coe_mul (x y : ℝ) :
↑x * y = (↑x) * ↑y

source
@[simp]
theorem hyperreal.coe_div (x y : ℝ) :
↑(x / y) = ↑x / ↑y

source
@[simp]
theorem hyperreal.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y

source
@[simp]
theorem hyperreal.coe_lt_coe {x y : ℝ} :
↑x < ↑y ↔ x < y

source
@[simp]
theorem hyperreal.coe_pos {x : ℝ} :
0 < ↑x ↔ 0 < x

source
@[simp]
theorem hyperreal.coe_le_coe {x y : ℝ} :
↑x ≤ ↑y ↔ x ≤ y

source
@[simp]
theorem hyperreal.coe_abs (x : ℝ) :
↑(abs x) = abs ↑x

source
@[simp]
theorem hyperreal.coe_max (x y : ℝ) :
↑(max x y) = max ↑x ↑y

source
@[simp]
theorem hyperreal.coe_min (x y : ℝ) :
↑(min x y) = min ↑x ↑y

source
def hyperreal.of_seq (f : ℕ → ℝ) :
ℝ*

Construct a hyperreal number from a sequence of real numbers.

Equations
source
def hyperreal.epsilon  :
ℝ*

A sample infinitesimal hyperreal

Equations
source
def hyperreal.omega  :
ℝ*

A sample infinite hyperreal

Equations
source
theorem hyperreal.epsilon_eq_inv_omega  :
hyperreal.epsilon = ω⁻¹

source
theorem hyperreal.inv_epsilon_eq_omega  :
hyperreal.epsilon⁻¹ = ω

source
theorem hyperreal.epsilon_pos  :
0 < hyperreal.epsilon

source
theorem hyperreal.epsilon_ne_zero  :
hyperreal.epsilon ≠ 0

source
theorem hyperreal.omega_pos  :
0 < ω

source
theorem hyperreal.omega_ne_zero  :
ω ≠ 0

source
theorem hyperreal.epsilon_mul_omega  :
hyperreal.epsilon * ω = 1

source
theorem hyperreal.lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top (𝓝 0)) {r : ℝ} (a : 0 < r) :
hyperreal.of_seq f < ↑r

source
theorem hyperreal.neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top (𝓝 0)) {r : ℝ} (a : 0 < r) :
-↑r < hyperreal.of_seq f

source
theorem hyperreal.gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top (𝓝 0)) {r : ℝ} (a : r < 0) :
↑r < hyperreal.of_seq f

source
theorem hyperreal.epsilon_lt_pos (x : ℝ) (a : 0 < x) :
hyperreal.epsilon < ↑x

source
def hyperreal.is_st (x : ℝ*) (r : ℝ) :
Prop

Standard part predicate

Equations
source
def hyperreal.st (a : ℝ*) :
ℝ

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

Equations
source
def hyperreal.infinitesimal (x : ℝ*) :
Prop

A hyperreal number is infinitesimal if its standard part is 0

Equations
source
def hyperreal.infinite_pos (x : ℝ*) :
Prop

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

Equations
source
def hyperreal.infinite_neg (x : ℝ*) :
Prop

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

Equations
source
def hyperreal.infinite (x : ℝ*) :
Prop

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

Equations

Some facts about st

source
theorem hyperreal.is_st_unique {x : ℝ*} {r s : ℝ} (hr : x.is_st r) (hs : x.is_st s) :
r = s

source
theorem hyperreal.not_infinite_of_exists_st {x : ℝ*} (a : ∃ (r : ℝ), x.is_st r) :
¬x.infinite

source
theorem hyperreal.is_st_Sup {x : ℝ*} (hni : ¬x.infinite) :
x.is_st (Sup {y : ℝ | ↑y < x})

source
theorem hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬x.infinite) :
∃ (r : ℝ), x.is_st r

source
theorem hyperreal.st_eq_Sup {x : ℝ*} :
x.st = Sup {y : ℝ | ↑y < x}

source
theorem hyperreal.exists_st_iff_not_infinite {x : ℝ*} :
(∃ (r : ℝ), x.is_st r) ↔ ¬x.infinite

source
theorem hyperreal.infinite_iff_not_exists_st {x : ℝ*} :
x.infinite ↔ ¬∃ (r : ℝ), x.is_st r

source
theorem hyperreal.st_infinite {x : ℝ*} (hi : x.infinite) :
x.st = 0

source
theorem hyperreal.st_of_is_st {x : ℝ*} {r : ℝ} (hxr : x.is_st r) :
x.st = r

source
theorem hyperreal.is_st_st_of_is_st {x : ℝ*} {r : ℝ} (hxr : x.is_st r) :
x.is_st x.st

source
theorem hyperreal.is_st_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ℝ), x.is_st r) :
x.is_st x.st

source
theorem hyperreal.is_st_st {x : ℝ*} (hx : x.st ≠ 0) :
x.is_st x.st

source
theorem hyperreal.is_st_st' {x : ℝ*} (hx : ¬x.infinite) :
x.is_st x.st

source
theorem hyperreal.is_st_refl_real (r : ℝ) :
↑r.is_st r

source
theorem hyperreal.st_id_real (r : ℝ) :
↑r.st = r

source
theorem hyperreal.eq_of_is_st_real {r s : ℝ} (a : ↑r.is_st s) :
r = s

source
theorem hyperreal.is_st_real_iff_eq {r s : ℝ} :
↑r.is_st s ↔ r = s

source
theorem hyperreal.is_st_symm_real {r s : ℝ} :
↑r.is_st s ↔ ↑s.is_st r

source
theorem hyperreal.is_st_trans_real {r s t : ℝ} (a : ↑r.is_st s) (a_1 : ↑s.is_st t) :
↑r.is_st t

source
theorem hyperreal.is_st_inj_real {r₁ r₂ s : ℝ} (h1 : ↑r₁.is_st s) (h2 : ↑r₂.is_st s) :
r₁ = r₂

source
theorem hyperreal.is_st_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} :
x.is_st r ↔ ∀ (δ : ℝ), 0 < δ → abs (x - ↑r) < ↑δ

source
theorem hyperreal.is_st_add {x y : ℝ*} {r s : ℝ} (a : x.is_st r) (a_1 : y.is_st s) :
(x + y).is_st (r + s)

source
theorem hyperreal.is_st_neg {x : ℝ*} {r : ℝ} (hxr : x.is_st r) :
(-x).is_st (-r)

source
theorem hyperreal.is_st_sub {x y : ℝ*} {r s : ℝ} (a : x.is_st r) (a_1 : y.is_st s) :
(x - y).is_st (r - s)

source
theorem hyperreal.lt_of_is_st_lt {x y : ℝ*} {r s : ℝ} (hxr : x.is_st r) (hys : y.is_st s) (a : r < s) :
x < y

source
theorem hyperreal.is_st_le_of_le {x y : ℝ*} {r s : ℝ} (hrx : x.is_st r) (hsy : y.is_st s) (a : x ≤ y) :
r ≤ s

source
theorem hyperreal.st_le_of_le {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) (a : x ≤ y) :
x.st ≤ y.st

source
theorem hyperreal.lt_of_st_lt {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) (a : x.st < y.st) :
x < y

Basic lemmas about infinite

source
theorem hyperreal.infinite_pos_def {x : ℝ*} :
x.infinite_pos ↔ ∀ (r : ℝ), ↑r < x

source
theorem hyperreal.infinite_neg_def {x : ℝ*} :
x.infinite_neg ↔ ∀ (r : ℝ), x < ↑r

source
theorem hyperreal.ne_zero_of_infinite {x : ℝ*} (a : x.infinite) :
x ≠ 0

source
theorem hyperreal.not_infinite_zero  :
¬0.infinite

source
theorem hyperreal.pos_of_infinite_pos {x : ℝ*} (a : x.infinite_pos) :
0 < x

source
theorem hyperreal.neg_of_infinite_neg {x : ℝ*} (a : x.infinite_neg) :
x < 0

source
theorem hyperreal.not_infinite_pos_of_infinite_neg {x : ℝ*} (a : x.infinite_neg) :
¬x.infinite_pos

source
theorem hyperreal.not_infinite_neg_of_infinite_pos {x : ℝ*} (a : x.infinite_pos) :
¬x.infinite_neg

source
theorem hyperreal.infinite_neg_neg_of_infinite_pos {x : ℝ*} (a : x.infinite_pos) :
(-x).infinite_neg

source
theorem hyperreal.infinite_pos_neg_of_infinite_neg {x : ℝ*} (a : x.infinite_neg) :
(-x).infinite_pos

source
theorem hyperreal.infinite_pos_iff_infinite_neg_neg {x : ℝ*} :
x.infinite_pos ↔ (-x).infinite_neg

source
theorem hyperreal.infinite_neg_iff_infinite_pos_neg {x : ℝ*} :
x.infinite_neg ↔ (-x).infinite_pos

source
theorem hyperreal.infinite_iff_infinite_neg {x : ℝ*} :
x.infinite ↔ (-x).infinite

source
theorem hyperreal.not_infinite_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) :
¬x.infinite

source
theorem hyperreal.not_infinitesimal_of_infinite {x : ℝ*} (a : x.infinite) :
¬x.infinitesimal

source
theorem hyperreal.not_infinitesimal_of_infinite_pos {x : ℝ*} (a : x.infinite_pos) :
¬x.infinitesimal

source
theorem hyperreal.not_infinitesimal_of_infinite_neg {x : ℝ*} (a : x.infinite_neg) :
¬x.infinitesimal

source
theorem hyperreal.infinite_pos_iff_infinite_and_pos {x : ℝ*} :
x.infinite_pos ↔ x.infinite ∧ 0 < x

source
theorem hyperreal.infinite_neg_iff_infinite_and_neg {x : ℝ*} :
x.infinite_neg ↔ x.infinite ∧ x < 0

source
theorem hyperreal.infinite_pos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) :
x.infinite_pos ↔ x.infinite

source
theorem hyperreal.infinite_pos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 ≤ x) :
x.infinite_pos ↔ x.infinite

source
theorem hyperreal.infinite_neg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) :
x.infinite_neg ↔ x.infinite

source
theorem hyperreal.infinite_pos_abs_iff_infinite_abs {x : ℝ*} :
(abs x).infinite_pos ↔ (abs x).infinite

source
theorem hyperreal.infinite_iff_infinite_pos_abs {x : ℝ*} :
x.infinite ↔ (abs x).infinite_pos

source
theorem hyperreal.infinite_iff_infinite_abs {x : ℝ*} :
x.infinite ↔ (abs x).infinite

source
theorem hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} :
x.infinite ↔ ∀ (r : ℝ), abs ↑r < abs x

source
theorem hyperreal.infinite_pos_add_not_infinite_neg {x y : ℝ*} (a : x.infinite_pos) (a_1 : ¬y.infinite_neg) :
(x + y).infinite_pos

source
theorem hyperreal.not_infinite_neg_add_infinite_pos {x y : ℝ*} (a : ¬x.infinite_neg) (a_1 : y.infinite_pos) :
(x + y).infinite_pos

source
theorem hyperreal.infinite_neg_add_not_infinite_pos {x y : ℝ*} (a : x.infinite_neg) (a_1 : ¬y.infinite_pos) :
(x + y).infinite_neg

source
theorem hyperreal.not_infinite_pos_add_infinite_neg {x y : ℝ*} (a : ¬x.infinite_pos) (a_1 : y.infinite_neg) :
(x + y).infinite_neg

source
theorem hyperreal.infinite_pos_add_infinite_pos {x y : ℝ*} (a : x.infinite_pos) (a_1 : y.infinite_pos) :
(x + y).infinite_pos

source
theorem hyperreal.infinite_neg_add_infinite_neg {x y : ℝ*} (a : x.infinite_neg) (a_1 : y.infinite_neg) :
(x + y).infinite_neg

source
theorem hyperreal.infinite_pos_add_not_infinite {x y : ℝ*} (a : x.infinite_pos) (a_1 : ¬y.infinite) :
(x + y).infinite_pos

source
theorem hyperreal.infinite_neg_add_not_infinite {x y : ℝ*} (a : x.infinite_neg) (a_1 : ¬y.infinite) :
(x + y).infinite_neg

source
theorem hyperreal.infinite_pos_of_tendsto_top {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top filter.at_top) :
(hyperreal.of_seq f).infinite_pos

source
theorem hyperreal.infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top filter.at_bot) :
(hyperreal.of_seq f).infinite_neg

source
theorem hyperreal.not_infinite_neg {x : ℝ*} (a : ¬x.infinite) :
¬(-x).infinite

source
theorem hyperreal.not_infinite_add {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
¬(x + y).infinite

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

source
theorem hyperreal.not_infinite_real (r : ℝ) :
¬↑r.infinite

source
theorem hyperreal.not_real_of_infinite {x : ℝ*} (a : x.infinite) (r : ℝ) :
x ≠ ↑r

Facts about st that require some infinite machinery

source
theorem hyperreal.is_st_mul {x y : ℝ*} {r s : ℝ} (hxr : x.is_st r) (hys : y.is_st s) :
(x * y).is_st (r * s)

source
theorem hyperreal.not_infinite_mul {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
¬(x * y).infinite

source
theorem hyperreal.st_add {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
(x + y).st = x.st + y.st

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

source
theorem hyperreal.st_mul {x y : ℝ*} (hx : ¬x.infinite) (hy : ¬y.infinite) :
(x * y).st = (x.st) * y.st

Basic lemmas about infinitesimal

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

source
theorem hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ℝ) (a_1 : 0 < r) :
x < ↑r

source
theorem hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ℝ) (a_1 : 0 < r) :
-↑r < x

source
theorem hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ℝ) (a_1 : r < 0) :
↑r < x

source
theorem hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} :
x.infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → abs x < abs ↑r

source
theorem hyperreal.infinitesimal_zero  :
0.infinitesimal

source
theorem hyperreal.zero_of_infinitesimal_real {r : ℝ} (a : ↑r.infinitesimal) :
r = 0

source
theorem hyperreal.zero_iff_infinitesimal_real {r : ℝ} :
↑r.infinitesimal ↔ r = 0

source
theorem hyperreal.infinitesimal_add {x y : ℝ*} (hx : x.infinitesimal) (hy : y.infinitesimal) :
(x + y).infinitesimal

source
theorem hyperreal.infinitesimal_neg {x : ℝ*} (hx : x.infinitesimal) :
(-x).infinitesimal

source
theorem hyperreal.infinitesimal_neg_iff {x : ℝ*} :
x.infinitesimal ↔ (-x).infinitesimal

source
theorem hyperreal.infinitesimal_mul {x y : ℝ*} (hx : x.infinitesimal) (hy : y.infinitesimal) :
(x * y).infinitesimal

source
theorem hyperreal.infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (a : filter.tendsto f filter.at_top (𝓝 0)) :
(hyperreal.of_seq f).infinitesimal

source
theorem hyperreal.infinitesimal_epsilon  :
hyperreal.epsilon.infinitesimal

source
theorem hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) (a : x.infinitesimal) (a_1 : x ≠ 0) (r : ℝ) :
x ≠ ↑r

source
theorem hyperreal.infinitesimal_sub_is_st {x : ℝ*} {r : ℝ} (hxr : x.is_st r) :
(x - ↑r).infinitesimal

source
theorem hyperreal.infinitesimal_sub_st {x : ℝ*} (hx : ¬x.infinite) :
(x - ↑(x.st)).infinitesimal

source
theorem hyperreal.infinite_pos_iff_infinitesimal_inv_pos {x : ℝ*} :
x.infinite_pos ↔ x⁻¹.infinitesimal ∧ 0 < x⁻¹

source
theorem hyperreal.infinite_neg_iff_infinitesimal_inv_neg {x : ℝ*} :
x.infinite_neg ↔ x⁻¹.infinitesimal ∧ x⁻¹ < 0

source
theorem hyperreal.infinitesimal_inv_of_infinite {x : ℝ*} (a : x.infinite) :
x⁻¹.infinitesimal

source
theorem hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : x⁻¹.infinitesimal) :
x.infinite

source
theorem hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) :
x.infinite ↔ x⁻¹.infinitesimal

source
theorem hyperreal.infinitesimal_pos_iff_infinite_pos_inv {x : ℝ*} :
x⁻¹.infinite_pos ↔ x.infinitesimal ∧ 0 < x

source
theorem hyperreal.infinitesimal_neg_iff_infinite_neg_inv {x : ℝ*} :
x⁻¹.infinite_neg ↔ x.infinitesimal ∧ x < 0

source
theorem hyperreal.infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) :
x.infinitesimal ↔ x⁻¹.infinite

st stuff that requires infinitesimal machinery

source
theorem hyperreal.is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : filter.tendsto f filter.at_top (𝓝 r)) :
(hyperreal.of_seq f).is_st r

source
theorem hyperreal.is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬x.infinitesimal) (a : x.is_st r) :
x⁻¹.is_st r⁻¹

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

Infinite stuff that requires infinitesimal machinery

source
theorem hyperreal.infinite_pos_omega  :
ω.infinite_pos

source
theorem hyperreal.infinite_omega  :
ω.infinite

source
theorem hyperreal.infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos {x y : ℝ*} (a : x.infinite_pos) (a_1 : ¬y.infinitesimal) (a_2 : 0 < y) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_pos_mul_of_not_infinitesimal_pos_infinite_pos {x y : ℝ*} (a : ¬x.infinitesimal) (a_1 : 0 < x) (a_2 : y.infinite_pos) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg {x y : ℝ*} (a : x.infinite_neg) (a_1 : ¬y.infinitesimal) (a_2 : y < 0) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_pos_mul_of_not_infinitesimal_neg_infinite_neg {x y : ℝ*} (a : ¬x.infinitesimal) (a_1 : x < 0) (a_2 : y.infinite_neg) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg {x y : ℝ*} (a : x.infinite_pos) (a_1 : ¬y.infinitesimal) (a_2 : y < 0) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_neg_mul_of_not_infinitesimal_neg_infinite_pos {x y : ℝ*} (a : ¬x.infinitesimal) (a_1 : x < 0) (a_2 : y.infinite_pos) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos {x y : ℝ*} (a : x.infinite_neg) (a_1 : ¬y.infinitesimal) (a_2 : 0 < y) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg {x y : ℝ*} (a : ¬x.infinitesimal) (a_1 : 0 < x) (a_2 : y.infinite_neg) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_pos_mul_infinite_pos {x y : ℝ*} (a : x.infinite_pos) (a_1 : y.infinite_pos) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_neg_mul_infinite_neg {x y : ℝ*} (a : x.infinite_neg) (a_1 : y.infinite_neg) :
(x * y).infinite_pos

source
theorem hyperreal.infinite_pos_mul_infinite_neg {x y : ℝ*} (a : x.infinite_pos) (a_1 : y.infinite_neg) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_neg_mul_infinite_pos {x y : ℝ*} (a : x.infinite_neg) (a_1 : y.infinite_pos) :
(x * y).infinite_neg

source
theorem hyperreal.infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} (a : x.infinite) (a_1 : ¬y.infinitesimal) :
(x * y).infinite

source
theorem hyperreal.infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} (a : ¬x.infinitesimal) (a_1 : y.infinite) :
(x * y).infinite

source
theorem hyperreal.infinite_mul_infinite {x y : ℝ*} (a : x.infinite) (a_1 : y.infinite) :
(x * y).infinite