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

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances For

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances For
Equations

Natural embedding ℝ → ℝ*.

Equations
Instances For
noncomputable instance Hyperreal.instCoeTCRealHyperreal :
Equations
@[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 : ) [] :
() =
@[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
• = f
Instances For
theorem Hyperreal.ofSeq_lt_ofSeq {f : } {g : } :
∀ᶠ (n : ) in , f n < g n
noncomputable def Hyperreal.epsilon :

A sample infinitesimal hyperreal

Equations
Instances For
noncomputable def Hyperreal.omega :

A sample infinite hyperreal

Equations
Instances For

A sample infinitesimal hyperreal

Equations
Instances For

A sample infinite hyperreal

Equations
Instances For
@[simp]
@[simp]
theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < r < r
theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
0 < r
theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
r < 0r <
theorem Hyperreal.epsilon_lt_pos (x : ) :
0 < x
def Hyperreal.IsSt (x : ℝ*) (r : ) :

Standard part predicate

Equations
• = ∀ (δ : ), 0 < δr - δ < x x < r + δ
Instances For
noncomputable def Hyperreal.st :
ℝ*

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

Equations
• = if h : ∃ (r : ), then else 0
Instances For

A hyperreal number is infinitesimal if its standard part is 0

Equations
Instances For

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

Equations
• = ∀ (r : ), r < x
Instances For

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

Equations
• = ∀ (r : ), x < r
Instances For

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

Equations
Instances For

theorem Hyperreal.isSt_of_tendsto {f : } {r : } (hf : Filter.Tendsto f Filter.atTop (nhds r)) :
theorem Hyperreal.IsSt.lt {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : ) (hys : ) (hrs : r < s) :
x < y
theorem Hyperreal.IsSt.unique {x : ℝ*} {r : } {s : } (hr : ) (hs : ) :
r = s
theorem Hyperreal.IsSt.st_eq {x : ℝ*} {r : } (hxr : ) :
theorem Hyperreal.IsSt.not_infinite {x : ℝ*} {r : } (h : ) :
theorem Hyperreal.not_infinite_of_exists_st {x : ℝ*} :
(∃ (r : ), )
theorem Hyperreal.Infinite.st_eq {x : ℝ*} (hi : ) :
theorem Hyperreal.isSt_sSup {x : ℝ*} (hni : ) :
Hyperreal.IsSt x (sSup {y : | y < x})
theorem Hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ) :
∃ (r : ),
theorem Hyperreal.st_eq_sSup {x : ℝ*} :
= sSup {y : | y < x}
theorem Hyperreal.IsSt.isSt_st {x : ℝ*} {r : } (hxr : ) :
theorem Hyperreal.isSt_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ), ) :
theorem Hyperreal.isSt_st' {x : ℝ*} (hx : ) :
theorem Hyperreal.isSt_st {x : ℝ*} (hx : ) :
theorem Hyperreal.st_id_real (r : ) :
= r
theorem Hyperreal.eq_of_isSt_real {r : } {s : } :
Hyperreal.IsSt (r) sr = s
theorem Hyperreal.isSt_real_iff_eq {r : } {s : } :
Hyperreal.IsSt (r) s r = s
theorem Hyperreal.isSt_trans_real {r : } {s : } {t : } :
Hyperreal.IsSt (r) sHyperreal.IsSt (s) tHyperreal.IsSt (r) t
theorem Hyperreal.isSt_inj_real {r₁ : } {r₂ : } {s : } (h1 : Hyperreal.IsSt (r₁) s) (h2 : Hyperreal.IsSt (r₂) s) :
r₁ = r₂
theorem Hyperreal.isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : } :
∀ (δ : ), 0 < δ|x - r| < δ
theorem Hyperreal.IsSt.map {x : ℝ*} {r : } (hxr : ) {f : } (hf : ) :
theorem Hyperreal.IsSt.map₂ {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : ) (hys : ) {f : } (hf : ContinuousAt () (r, s)) :
Hyperreal.IsSt () (f r s)
theorem Hyperreal.IsSt.add {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : ) (hys : ) :
Hyperreal.IsSt (x + y) (r + s)
theorem Hyperreal.IsSt.neg {x : ℝ*} {r : } (hxr : ) :
theorem Hyperreal.IsSt.sub {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : ) (hys : ) :
Hyperreal.IsSt (x - y) (r - s)
theorem Hyperreal.IsSt.le {x : ℝ*} {y : ℝ*} {r : } {s : } (hrx : ) (hsy : ) (hxy : x y) :
r s
theorem Hyperreal.st_le_of_le {x : ℝ*} {y : ℝ*} (hix : ) (hiy : ) :
x y
theorem Hyperreal.lt_of_st_lt {x : ℝ*} {y : ℝ*} (hix : ) (hiy : ) :
x < y

### Basic lemmas about infinite #

theorem Hyperreal.infinitePos_def {x : ℝ*} :
∀ (r : ), r < x
theorem Hyperreal.infiniteNeg_def {x : ℝ*} :
∀ (r : ), x < r
theorem Hyperreal.InfinitePos.pos {x : ℝ*} (hip : ) :
0 < x
theorem Hyperreal.Infinite.ne_zero {x : ℝ*} (hI : ) :
x 0
@[simp]
@[simp]
@[simp]
@[simp]
theorem Hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} :
∀ (r : ), |r| < |x|
theorem Hyperreal.infinitePos_of_tendsto_top {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atTop) :
theorem Hyperreal.infiniteNeg_of_tendsto_bot {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atBot) :
theorem Hyperreal.not_infinite_add {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :
theorem Hyperreal.not_infinite_iff_exist_lt_gt {x : ℝ*} :
∃ (r : ) (s : ), r < x x < s
theorem Hyperreal.Infinite.ne_real {x : ℝ*} :
∀ (r : ), x r

### Facts about st that require some infinite machinery #

theorem Hyperreal.IsSt.mul {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : ) (hys : ) :
Hyperreal.IsSt (x * y) (r * s)
theorem Hyperreal.not_infinite_mul {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :
theorem Hyperreal.st_add {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :
theorem Hyperreal.st_mul {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :

### Basic lemmas about infinitesimal #

theorem Hyperreal.infinitesimal_def {x : ℝ*} :
∀ (r : ), 0 < r-r < x x < r
theorem Hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} :
∀ (r : ), 0 < rx < r
theorem Hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} :
∀ (r : ), 0 < r-r < x
theorem Hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (hi : ) (r : ) (hr : r < 0) :
r < x
theorem Hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} :
∀ (r : ), r 0|x| < |r|
@[simp]
theorem Hyperreal.Infinitesimal.add {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :
theorem Hyperreal.Infinitesimal.neg {x : ℝ*} (hx : ) :
@[simp]
theorem Hyperreal.Infinitesimal.mul {x : ℝ*} {y : ℝ*} (hx : ) (hy : ) :
theorem Hyperreal.infinitesimal_of_tendsto_zero {f : } (h : Filter.Tendsto f Filter.atTop (nhds 0)) :
theorem Hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) :
x 0∀ (r : ), x r
theorem Hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x 0) (hi : ) :

### Hyperreal.st stuff that requires infinitesimal machinery #

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

### Infinite stuff that requires infinitesimal machinery #

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