mathlib docs: data.real.hyperreal

source

def hyperreal :

Type

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations

ℝ* = filter.hyperfilter.germ ℝ

source

@[instance]

def hyperreal.discrete_linear_ordered_field :

discrete_linear_ordered_field ℝ*

Equations

hyperreal.discrete_linear_ordered_field = filter.germ.discrete_linear_ordered_field U

source

@[instance]

def hyperreal.inhabited :

inhabited ℝ*

Equations

hyperreal.inhabited = {default := 0}

source

@[instance]

def hyperreal.has_coe_t :

has_coe_t ℝ ℝ*

Equations

hyperreal.has_coe_t = {coe := λ (x : ℝ), ↑x}

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 :

(ℕ → ℝ) → ℝ*

Construct a hyperreal number from a sequence of real numbers.

Equations

hyperreal.of_seq f = ↑f

source

def hyperreal.epsilon :

ℝ*

A sample infinitesimal hyperreal

Equations

hyperreal.epsilon = hyperreal.of_seq (λ (n : ℕ), (↑n)⁻¹)

source

def hyperreal.omega :

ℝ*

A sample infinite hyperreal

Equations

hyperreal.omega = hyperreal.of_seq coe

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 :

ℝ* → ℝ → Prop

Standard part predicate

Equations

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

source

def hyperreal.st :

ℝ* → ℝ

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

Equations

hyperreal.st = λ (x : ℝ*), dite (∃ (r : ℝ), x.is_st r) (λ (h : ∃ (r : ℝ), x.is_st r), classical.some h) (λ (h : ¬∃ (r : ℝ), x.is_st r), 0)

source

def hyperreal.infinitesimal :

ℝ* → Prop

A hyperreal number is infinitesimal if its standard part is 0

Equations

x.infinitesimal = x.is_st 0

source

def hyperreal.infinite_pos :

ℝ* → Prop

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

Equations

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

source

def hyperreal.infinite_neg :

ℝ* → Prop

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

Equations

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

source

def hyperreal.infinite :

ℝ* → Prop

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

Equations

x.infinite = (x.infinite_pos ∨ x.infinite_neg)

source

theorem hyperreal.is_st_unique {x : ℝ*} {r s : ℝ} :

x.is_st r → 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 : ℝ*} :

¬x.infinite → x.is_st (has_Sup.Sup {y : ℝ | ↑y < x})

source

theorem hyperreal.exists_st_of_not_infinite {x : ℝ*} :

¬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 : ℝ*} :

x.infinite → x.st = 0

source

theorem hyperreal.st_of_is_st {x : ℝ*} {r : ℝ} :

x.is_st r → x.st = r

source

theorem hyperreal.is_st_st_of_is_st {x : ℝ*} {r : ℝ} :

x.is_st r → x.is_st x.st

source

theorem hyperreal.is_st_st_of_exists_st {x : ℝ*} :

(∃ (r : ℝ), x.is_st r) → x.is_st x.st

source

theorem hyperreal.is_st_st {x : ℝ*} :

x.st ≠ 0 → x.is_st x.st

source

theorem hyperreal.is_st_st' {x : ℝ*} :

¬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 : ℝ} :

↑r₁.is_st s → ↑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 : ℝ} :

x.is_st r → y.is_st s → (x + y).is_st (r + s)

source

theorem hyperreal.is_st_neg {x : ℝ*} {r : ℝ} :

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 : ℝ} :

x.is_st r → y.is_st s → r < s → x < y

source

theorem hyperreal.is_st_le_of_le {x y : ℝ*} {r s : ℝ} :

x.is_st r → y.is_st s → x ≤ y → r ≤ s

source

theorem hyperreal.st_le_of_le {x y : ℝ*} :

¬x.infinite → ¬y.infinite → x ≤ y → x.st ≤ y.st

source

theorem hyperreal.lt_of_st_lt {x y : ℝ*} :

¬x.infinite → ¬y.infinite → x.st < y.st → x < y

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 : ℝ*} :

0 < x → (x.infinite_pos ↔ x.infinite)

source

theorem hyperreal.infinite_pos_iff_infinite_of_nonneg {x : ℝ*} :

0 ≤ x → (x.infinite_pos ↔ x.infinite)

source

theorem hyperreal.infinite_neg_iff_infinite_of_neg {x : ℝ*} :

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 : ℝ*} :

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 : ℕ → ℝ} :

filter.tendsto f filter.at_top filter.at_top → (hyperreal.of_seq f).infinite_pos

source

theorem hyperreal.infinite_neg_of_tendsto_bot {f : ℕ → ℝ} :

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 : ℝ*} :

¬x.infinite → ¬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

source

theorem hyperreal.is_st_mul {x y : ℝ*} {r s : ℝ} :

x.is_st r → y.is_st s → (x * y).is_st (r * s)

source

theorem hyperreal.not_infinite_mul {x y : ℝ*} :

¬x.infinite → ¬y.infinite → ¬(x * y).infinite

source

theorem hyperreal.st_add {x y : ℝ*} :

¬x.infinite → ¬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 : ℝ*} :

¬x.infinite → ¬y.infinite → (x * y).st = x.st * y.st

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 : ℝ) :

0 < r → x < ↑r

source

theorem hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ℝ) :

0 < r → -↑r < x

source

theorem hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (a : x.infinitesimal) (r : ℝ) :

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 : ℝ} :

↑r.infinitesimal → r = 0

source

theorem hyperreal.zero_iff_infinitesimal_real {r : ℝ} :

↑r.infinitesimal ↔ r = 0

source

theorem hyperreal.infinitesimal_add {x y : ℝ*} :

x.infinitesimal → y.infinitesimal → (x + y).infinitesimal

source

theorem hyperreal.infinitesimal_neg {x : ℝ*} :

x.infinitesimal → (-x).infinitesimal

source

theorem hyperreal.infinitesimal_neg_iff {x : ℝ*} :

x.infinitesimal ↔ (-x).infinitesimal

source

theorem hyperreal.infinitesimal_mul {x y : ℝ*} :

x.infinitesimal → 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 : ℝ*) (a : x.infinitesimal) (a_1 : x ≠ 0) (r : ℝ) :

x ≠ ↑r

source

theorem hyperreal.infinitesimal_sub_is_st {x : ℝ*} {r : ℝ} :

x.is_st r → (x - ↑r).infinitesimal

source

theorem hyperreal.infinitesimal_sub_st {x : ℝ*} :

¬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 : ℝ*} :

x ≠ 0 → x⁻¹.infinitesimal → x.infinite

source

theorem hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} :

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 : ℝ*} :

x ≠ 0 → (x.infinitesimal ↔ x⁻¹.infinite)

source

theorem hyperreal.is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} :

filter.tendsto f filter.at_top (nhds r) → (hyperreal.of_seq f).is_st r

source

theorem hyperreal.is_st_inv {x : ℝ*} {r : ℝ} :

¬x.infinitesimal → x.is_st r → x⁻¹.is_st r⁻¹

source

theorem hyperreal.st_inv (x : ℝ*) :

x⁻¹.st = (x.st)⁻¹

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

mathlib documentation

data.real.hyperreal

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

Some facts about `st`

Basic lemmas about infinite

Facts about `st` that require some infinite machinery

Basic lemmas about infinitesimal

`st` stuff that requires infinitesimal machinery

Infinite stuff that requires infinitesimal machinery

General documentation

Additional documentation

Library

mathlib documentation

data.​real.​hyperreal

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

Some facts about st

Basic lemmas about infinite

Facts about st that require some infinite machinery

Basic lemmas about infinitesimal

st stuff that requires infinitesimal machinery

Infinite stuff that requires infinitesimal machinery

General documentation

Additional documentation

Library

data.real.hyperreal

Some facts about `st`

Facts about `st` that require some infinite machinery

`st` stuff that requires infinitesimal machinery