mathlib documentation

data.real.basic

structure real  :
Type

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

theorem real.ext_cauchy_iff {x y : } :
x = y x.cauchy = y.cauchy
theorem real.ext_cauchy {x y : } :
x.cauchy = y.cauchyx = y

The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem real.zero_cauchy  :
0⟩ = 0
theorem real.one_cauchy  :
1⟩ = 1
theorem real.add_cauchy {a b : cau_seq.completion.Cauchy} :
a⟩ + b⟩ = a + b
theorem real.neg_cauchy {a : cau_seq.completion.Cauchy} :
-a⟩ = -a⟩
theorem real.mul_cauchy {a b : cau_seq.completion.Cauchy} :
a⟩ * b⟩ = a * b
@[instance]
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
theorem real.mk_eq {f g : cau_seq abs} :
@[instance]
Equations
theorem real.lt_cauchy {f g : cau_seq abs} :
f< g f < g
@[simp]
theorem real.mk_lt {f g : cau_seq abs} :
theorem real.mk_zero  :
theorem real.mk_one  :
theorem real.mk_add {f g : cau_seq abs} :
theorem real.mk_mul {f g : cau_seq abs} :
real.mk (f * g) = (real.mk f) * real.mk g
theorem real.mk_neg {f : cau_seq abs} :
@[simp]
theorem real.mk_pos {f : cau_seq abs} :
@[instance]
Equations
@[simp]
theorem real.mk_le {f g : cau_seq abs} :
theorem real.ind_mk {C : → Prop} (x : ) (h : ∀ (y : cau_seq abs), C (real.mk y)) :
C x
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]

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

Equations
@[instance]
Equations
theorem real.inv_cauchy {f : cau_seq.completion.Cauchy} :
f⟩⁻¹ = f⁻¹
@[instance]
Equations
@[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 : } (h : ∃ (i : ), ∀ (j : ), j i(f j) 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