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
Instances for hyperreal
source
@[protected, instance]
noncomputable def hyperreal.inhabited  :
inhabited ℝ*
source
@[protected, instance]
noncomputable def hyperreal.linear_ordered_field  :
linear_ordered_field ℝ*
source
@[protected, instance]
noncomputable def hyperreal.has_coe_t  :
has_coe_t ℝ ℝ*
Equations
source
@[simp, norm_cast]
theorem hyperreal.coe_eq_coe {x y : ℝ} :
↑x = ↑y ↔ x = y
source
@[simp, norm_cast]
theorem hyperreal.coe_eq_zero {x : ℝ} :
↑x = 0 ↔ x = 0
source
@[simp, norm_cast]
theorem hyperreal.coe_eq_one {x : ℝ} :
↑x = 1 ↔ x = 1
source
@[simp, norm_cast]
theorem hyperreal.coe_one  :
↑1 = 1
source
@[simp, norm_cast]
theorem hyperreal.coe_zero  :
↑0 = 0
source
@[simp, norm_cast]
theorem hyperreal.coe_inv (x : ℝ) :
↑x⁻¹ = (↑x)⁻¹
source
@[simp, norm_cast]
theorem hyperreal.coe_neg (x : ℝ) :
↑-x = -↑x
source
@[simp, norm_cast]
theorem hyperreal.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y
source
@[simp, norm_cast]
theorem hyperreal.coe_bit0 (x : ℝ) :
↑(bit0 x) = bit0 ↑x
source
@[simp, norm_cast]
theorem hyperreal.coe_bit1 (x : ℝ) :
↑(bit1 x) = bit1 ↑x
source
@[simp, norm_cast]
theorem hyperreal.coe_mul (x y : ℝ) :
↑(x * y) = ↑x * ↑y
source
@[simp, norm_cast]
theorem hyperreal.coe_div (x y : ℝ) :
↑(x / y) = ↑x / ↑y
source
@[simp, norm_cast]
theorem hyperreal.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y
source
@[simp, norm_cast]
theorem hyperreal.coe_lt_coe {x y : ℝ} :
↑x < ↑y ↔ x < y
source
@[simp, norm_cast]
theorem hyperreal.coe_pos {x : ℝ} :
0 < ↑x ↔ 0 < x
source
@[simp, norm_cast]
theorem hyperreal.coe_le_coe {x y : ℝ} :
↑x ≤ ↑y ↔ x ≤ y
source
@[simp, norm_cast]
theorem hyperreal.coe_abs (x : ℝ) :
↑|x| = |↑x|
source
@[simp, norm_cast]
theorem hyperreal.coe_max (x y : ℝ) :
↑(linear_order.max x y) = linear_order.max ↑x ↑y
source
@[simp, norm_cast]
theorem hyperreal.coe_min (x y : ℝ) :
↑(linear_order.min x y) = linear_order.min ↑x ↑y
source
noncomputable def hyperreal.of_seq (f : ℕ → ℝ) :
ℝ*

Construct a hyperreal number from a sequence of real numbers.

Equations
source
noncomputable def hyperreal.epsilon  :
ℝ*

A sample infinitesimal hyperreal

Equations
source
noncomputable def hyperreal.omega  :
ℝ*

A sample infinite hyperreal

Equations
source
theorem hyperreal.epsilon_eq_inv_omega  :
hyperreal.epsilon = hyperreal.omega⁻¹
source
theorem hyperreal.inv_epsilon_eq_omega  :
hyperreal.epsilon⁻¹ = hyperreal.omega
source
theorem hyperreal.epsilon_pos  :
0 < hyperreal.epsilon
source
theorem hyperreal.epsilon_ne_zero  :
hyperreal.epsilon ≠ 0
source
theorem hyperreal.omega_pos  :
0 < hyperreal.omega
source
theorem hyperreal.omega_ne_zero  :
hyperreal.omega ≠ 0
source
theorem hyperreal.epsilon_mul_omega  :
hyperreal.epsilon * hyperreal.omega = 1
source
theorem hyperreal.lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top (nhds 0)) {r : ℝ} :
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 (nhds 0)) {r : ℝ} :
0 < r → -↑r < hyperreal.of_seq f
source
theorem hyperreal.gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : filter.tendsto f filter.at_top (nhds 0)) {r : ℝ} :
r < 0 → ↑r < hyperreal.of_seq f
source
theorem hyperreal.epsilon_lt_pos (x : ℝ) :
0 < x → hyperreal.epsilon < ↑x
source
def hyperreal.is_st (x : ℝ*) (r : ℝ) :
Prop

Standard part predicate

Equations
source
noncomputable def hyperreal.st  :
ℝ* → ℝ

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 : ℝ*} :
(∃ (r : ℝ), x.is_st r) → ¬x.infinite
source
theorem hyperreal.is_st_Sup {x : ℝ*} (hni : ¬x.infinite) :
x.is_st (has_Sup.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 = has_Sup.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 : ℝ} :
↑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 : ℝ} :
↑r.is_st s → ↑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 < δ → |x - ↑r| < ↑δ
source
theorem hyperreal.is_st_add {x y : ℝ*} {r s : ℝ} :
x.is_st r → 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 : ℝ} :
x.is_st r → 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) :
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) :
x ≤ y → r ≤ s
source
theorem hyperreal.st_le_of_le {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
x ≤ y → x.st ≤ y.st
source
theorem hyperreal.lt_of_st_lt {x y : ℝ*} (hix : ¬x.infinite) (hiy : ¬y.infinite) :
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 : ℝ*} :
x.infinite → x ≠ 0
source
theorem hyperreal.not_infinite_zero  :
¬0.infinite
source
theorem hyperreal.pos_of_infinite_pos {x : ℝ*} :
x.infinite_pos → 0 < x
source
theorem hyperreal.neg_of_infinite_neg {x : ℝ*} :
x.infinite_neg → x < 0
source
theorem hyperreal.not_infinite_pos_of_infinite_neg {x : ℝ*} :
x.infinite_neg → ¬x.infinite_pos
source
theorem hyperreal.not_infinite_neg_of_infinite_pos {x : ℝ*} :
x.infinite_pos → ¬x.infinite_neg
source
theorem hyperreal.infinite_neg_neg_of_infinite_pos {x : ℝ*} :
x.infinite_pos → (-x).infinite_neg
source
theorem hyperreal.infinite_pos_neg_of_infinite_neg {x : ℝ*} :
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 : ℝ*} :
x.infinitesimal → ¬x.infinite
source
theorem hyperreal.not_infinitesimal_of_infinite {x : ℝ*} :
x.infinite → ¬x.infinitesimal
source
theorem hyperreal.not_infinitesimal_of_infinite_pos {x : ℝ*} :
x.infinite_pos → ¬x.infinitesimal
source
theorem hyperreal.not_infinitesimal_of_infinite_neg {x : ℝ*} :
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 : ℝ*} :
|x|.infinite_pos ↔ |x|.infinite
source
theorem hyperreal.infinite_iff_infinite_pos_abs {x : ℝ*} :
x.infinite ↔ |x|.infinite_pos
source
theorem hyperreal.infinite_iff_infinite_abs {x : ℝ*} :
x.infinite ↔ |x|.infinite
source
theorem hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} :
x.infinite ↔ ∀ (r : ℝ), |↑r| < |x|
source
theorem hyperreal.infinite_pos_add_not_infinite_neg {x y : ℝ*} :
x.infinite_pos → ¬y.infinite_neg → (x + y).infinite_pos
source
theorem hyperreal.not_infinite_neg_add_infinite_pos {x y : ℝ*} :
¬x.infinite_neg → y.infinite_pos → (x + y).infinite_pos
source
theorem hyperreal.infinite_neg_add_not_infinite_pos {x y : ℝ*} :
x.infinite_neg → ¬y.infinite_pos → (x + y).infinite_neg
source
theorem hyperreal.not_infinite_pos_add_infinite_neg {x y : ℝ*} :
¬x.infinite_pos → y.infinite_neg → (x + y).infinite_neg
source
theorem hyperreal.infinite_pos_add_infinite_pos {x y : ℝ*} :
x.infinite_pos → y.infinite_pos → (x + y).infinite_pos
source
theorem hyperreal.infinite_neg_add_infinite_neg {x y : ℝ*} :
x.infinite_neg → y.infinite_neg → (x + y).infinite_neg
source
theorem hyperreal.infinite_pos_add_not_infinite {x y : ℝ*} :
x.infinite_pos → ¬y.infinite → (x + y).infinite_pos
source
theorem hyperreal.infinite_neg_add_not_infinite {x y : ℝ*} :
x.infinite_neg → ¬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 : ℝ*} :
¬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 : ℝ*} :
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 : ℝ*} :
x.infinitesimal → ∀ (r : ℝ), 0 < r → x < ↑r
source
theorem hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} :
x.infinitesimal → ∀ (r : ℝ), 0 < r → -↑r < x
source
theorem hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} :
x.infinitesimal → ∀ (r : ℝ), r < 0 → ↑r < x
source
theorem hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} :
x.infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |↑r|
source
theorem hyperreal.infinitesimal_zero  :
0.infinitesimal
source
theorem hyperreal.zero_of_infinitesimal_real {r : ℝ} :
↑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 : ℕ → ℝ} :
filter.tendsto f filter.at_top (nhds 0) → (hyperreal.of_seq f).infinitesimal
source
theorem hyperreal.infinitesimal_epsilon  :
hyperreal.epsilon.infinitesimal
source
theorem hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) :
x.infinitesimal → 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 : ℝ*} :
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 (nhds r)) :
(hyperreal.of_seq f).is_st r
source
theorem hyperreal.is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬x.infinitesimal) :
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  :
hyperreal.omega.infinite_pos
source
theorem hyperreal.infinite_omega  :
hyperreal.omega.infinite
source
theorem hyperreal.infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos {x y : ℝ*} :
x.infinite_pos → ¬y.infinitesimal → 0 < y → (x * y).infinite_pos
source
theorem hyperreal.infinite_pos_mul_of_not_infinitesimal_pos_infinite_pos {x y : ℝ*} :
¬x.infinitesimal → 0 < x → y.infinite_pos → (x * y).infinite_pos
source
theorem hyperreal.infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg {x y : ℝ*} :
x.infinite_neg → ¬y.infinitesimal → y < 0 → (x * y).infinite_pos
source
theorem hyperreal.infinite_pos_mul_of_not_infinitesimal_neg_infinite_neg {x y : ℝ*} :
¬x.infinitesimal → x < 0 → y.infinite_neg → (x * y).infinite_pos
source
theorem hyperreal.infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg {x y : ℝ*} :
x.infinite_pos → ¬y.infinitesimal → y < 0 → (x * y).infinite_neg
source
theorem hyperreal.infinite_neg_mul_of_not_infinitesimal_neg_infinite_pos {x y : ℝ*} :
¬x.infinitesimal → x < 0 → y.infinite_pos → (x * y).infinite_neg
source
theorem hyperreal.infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos {x y : ℝ*} :
x.infinite_neg → ¬y.infinitesimal → 0 < y → (x * y).infinite_neg
source
theorem hyperreal.infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg {x y : ℝ*} :
¬x.infinitesimal → 0 < x → y.infinite_neg → (x * y).infinite_neg
source
theorem hyperreal.infinite_pos_mul_infinite_pos {x y : ℝ*} :
x.infinite_pos → y.infinite_pos → (x * y).infinite_pos
source
theorem hyperreal.infinite_neg_mul_infinite_neg {x y : ℝ*} :
x.infinite_neg → y.infinite_neg → (x * y).infinite_pos
source
theorem hyperreal.infinite_pos_mul_infinite_neg {x y : ℝ*} :
x.infinite_pos → y.infinite_neg → (x * y).infinite_neg
source
theorem hyperreal.infinite_neg_mul_infinite_pos {x y : ℝ*} :
x.infinite_neg → y.infinite_pos → (x * y).infinite_neg
source
theorem hyperreal.infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} :
x.infinite → ¬y.infinitesimal → (x * y).infinite
source
theorem hyperreal.infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} :
¬x.infinitesimal → y.infinite → (x * y).infinite
source
theorem hyperreal.infinite_mul_infinite {x y : ℝ*} :
x.infinite → y.infinite → (x * y).infinite