mathlib documentation

data.real.basic

def real  :
Type

The type of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.

Equations
@[instance]
def real.ring  :

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

The real numbers are a *-ring, with the trivial *-structure.

Equations

Coercion as a ring_hom. Note that this is cau_seq.completion.of_rat, not rat.cast.

Equations
def real.mk (x : cau_seq abs) :

Make a real number from a Cauchy sequence of rationals (by taking the equivalence class).

Equations
@[instance]

Equations
@[simp]
theorem real.mk_lt {f g : cau_seq abs} :

theorem real.mk_eq {f g : cau_seq abs} :

@[simp]
theorem real.mk_pos {f : cau_seq abs} :

def real.le (x y : ) :
Prop

Equations
@[instance]

Equations
@[simp]
theorem real.mk_le {f g : cau_seq abs} :

theorem real.add_lt_add_iff_left {a b : } (c : ) :
c + a < c + b a < b

@[instance]

Equations
theorem real.zero_lt_one  :
0 < 1

theorem real.mul_pos {a b : } :
0 < a0 < b0 < a * b

@[instance]

@[instance]
def real.decidable_lt (a b : ) :
decidable (a < b)

Equations
@[instance]
def real.decidable_le (a b : ) :

Equations
@[instance]
def real.decidable_eq (a b : ) :
decidable (a = b)

Equations
@[simp]

theorem real.le_mk_of_forall_le {x : } {f : cau_seq abs} :
(∃ (i : ), ∀ (j : ), j ix (f j))x real.mk f

theorem real.mk_le_of_forall_le {f : cau_seq abs} {x : } :
(∃ (i : ), ∀ (j : ), j i(f j) x)real.mk f x

theorem real.mk_near_of_forall_near {f : cau_seq abs} {x ε : } (H : ∃ (i : ), ∀ (j : ), j iabs ((f j) - x) ε) :
abs (real.mk f - x) ε

@[instance]

theorem real.is_cau_seq_iff_lift {f : } :
is_cau_seq abs f is_cau_seq abs (λ (i : ), (f i))

theorem real.of_near (f : ) (x : ) (h : ∀ (ε : ), ε > 0(∃ (i : ), ∀ (j : ), j iabs ((f j) - x) < ε)) :
∃ (h' : is_cau_seq abs f), real.mk f, h'⟩ = x

theorem real.exists_floor (x : ) :
∃ (ub : ), ub x ∀ (z : ), z xz ub

theorem real.exists_sup (S : set ) :
(∃ (x : ), x S)(∃ (x : ), ∀ (y : ), y Sy x)(∃ (x : ), ∀ (y : ), x y ∀ (z : ), z Sz y)

@[instance]

Equations
theorem real.Sup_def (S : set ) :
Sup S = dite ((∃ (x : ), x S) ∃ (x : ), ∀ (y : ), y Sy x) (λ (h : (∃ (x : ), x S) ∃ (x : ), ∀ (y : ), y Sy x), classical.some _) (λ (h : ¬((∃ (x : ), x S) ∃ (x : ), ∀ (y : ), y Sy x)), 0)

theorem real.Sup_le (S : set ) (h₁ : ∃ (x : ), x S) (h₂ : ∃ (x : ), ∀ (y : ), y Sy x) {y : } :
Sup S y ∀ (z : ), z Sz y

theorem real.lt_Sup (S : set ) (h₁ : ∃ (x : ), x S) (h₂ : ∃ (x : ), ∀ (y : ), y Sy x) {y : } :
y < Sup S ∃ (z : ) (H : z S), y < z

theorem real.le_Sup (S : set ) (h₂ : ∃ (x : ), ∀ (y : ), y Sy x) {x : } (xS : x S) :
x Sup S

theorem real.Sup_le_ub (S : set ) (h₁ : ∃ (x : ), x S) {ub : } (h₂ : ∀ (y : ), y Sy ub) :
Sup S ub

theorem real.is_lub_Sup {s : set } {a b : } (ha : a s) (hb : b upper_bounds s) :
is_lub s (Sup s)

@[instance]

Equations
theorem real.Inf_def (S : set ) :
Inf S = -Sup {x : | -x S}

theorem real.le_Inf (S : set ) (h₁ : ∃ (x : ), x S) (h₂ : ∃ (x : ), ∀ (y : ), y Sx y) {y : } :
y Inf S ∀ (z : ), z Sy z

theorem real.Inf_lt (S : set ) (h₁ : ∃ (x : ), x S) (h₂ : ∃ (x : ), ∀ (y : ), y Sx y) {y : } :
Inf S < y ∃ (z : ) (H : z S), z < y

theorem real.Inf_le (S : set ) (h₂ : ∃ (x : ), ∀ (y : ), y Sx y) {x : } (xS : x S) :
Inf S x

theorem real.lb_le_Inf (S : set ) (h₁ : ∃ (x : ), x S) {lb : } (h₂ : ∀ (y : ), y Slb y) :
lb Inf S

@[instance]

Equations
theorem real.Sup_empty  :

theorem real.Sup_of_not_bdd_above {s : set } (hs : ¬bdd_above s) :
Sup s = 0

theorem real.Inf_empty  :

theorem real.Inf_of_not_bdd_below {s : set } (hs : ¬bdd_below s) :
Inf s = 0

theorem real.cau_seq_converges (f : cau_seq abs) :
∃ (x : ), f cau_seq.const abs x