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

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

Equations
def real.mk  :

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  :
→ 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
theorem real.le_of_forall_epsilon_le {a b : } :
(∀ (ε : ), 0 < εa b + ε)a b

@[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 ε : } :
(∃ (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 : ) :
(∀ (ε : ), ε > 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 : } :
x Sx Sup S

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

theorem real.is_lub_Sup {s : set } {a b : } :
a sb upper_bounds sis_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 : } :
x SInf S x

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

@[instance]

Equations
theorem real.Sup_empty  :

theorem real.Sup_of_not_bdd_above {s : set } :
¬bdd_above sSup s = 0

theorem real.Inf_empty  :

theorem real.Inf_of_not_bdd_below {s : set } :
¬bdd_below sInf s = 0

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

theorem real.sqrt_exists {x : } :
0 x(∃ (y : ), 0 y y * y = x)

def real.sqrt_aux  :

Equations
def real.sqrt  :

The square root of a real number. This returns 0 for negative inputs.

Equations
theorem real.sqrt_prop (x : ) :

theorem real.sqrt_eq_zero_of_nonpos {x : } :
x 0real.sqrt x = 0

theorem real.sqrt_nonneg (x : ) :

@[simp]
theorem real.mul_self_sqrt {x : } :
0 x(real.sqrt x) * real.sqrt x = x

@[simp]
theorem real.sqrt_mul_self {x : } :
0 xreal.sqrt (x * x) = x

theorem real.sqrt_eq_iff_mul_self_eq {x y : } :
0 x0 y(real.sqrt x = y y * y = x)

@[simp]
theorem real.sqr_sqrt {x : } :
0 xreal.sqrt x ^ 2 = x

@[simp]
theorem real.sqrt_sqr {x : } :
0 xreal.sqrt (x ^ 2) = x

theorem real.sqrt_eq_iff_sqr_eq {x y : } :
0 x0 y(real.sqrt x = y y ^ 2 = x)

theorem real.sqrt_mul_self_eq_abs (x : ) :
real.sqrt (x * x) = abs x

theorem real.sqrt_sqr_eq_abs (x : ) :
real.sqrt (x ^ 2) = abs x

@[simp]
theorem real.sqrt_zero  :

@[simp]
theorem real.sqrt_one  :

@[simp]
theorem real.sqrt_le {x y : } :
0 x0 y(real.sqrt x real.sqrt y x y)

@[simp]
theorem real.sqrt_lt {x y : } :
0 x0 y(real.sqrt x < real.sqrt y x < y)

theorem real.sqrt_le_sqrt {x y : } :

theorem real.sqrt_le_left {x y : } :
0 y(real.sqrt x y x y ^ 2)

theorem real.le_sqrt {x y : } :
0 x0 y(x real.sqrt y x ^ 2 y)

theorem real.le_sqrt' {x y : } :
0 < x(x real.sqrt y x ^ 2 y)

theorem real.le_sqrt_of_sqr_le {x y : } :
x ^ 2 yx real.sqrt y

@[simp]
theorem real.sqrt_inj {x y : } :
0 x0 y(real.sqrt x = real.sqrt y x = y)

@[simp]
theorem real.sqrt_eq_zero {x : } :
0 x(real.sqrt x = 0 x = 0)

theorem real.sqrt_eq_zero' {x : } :
real.sqrt x = 0 x 0

@[simp]
theorem real.sqrt_pos {x : } :
0 < real.sqrt x 0 < x

@[simp]
theorem real.sqrt_mul' (x : ) {y : } :
0 yreal.sqrt (x * y) = (real.sqrt x) * real.sqrt y

@[simp]
theorem real.sqrt_mul {x : } (hx : 0 x) (y : ) :

@[simp]

@[simp]
theorem real.sqrt_div {x : } (hx : 0 x) (y : ) :