mathlib documentation

data.real.basic

Real numbers from Cauchy sequences #

This file defines as the type of equivalence classes of Cauchy sequences of rational numbers. This choice is motivated by how easy it is to prove that is a commutative ring, by simply lifting everything to .

structure real  :
Type

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

Instances for real
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
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem real.of_cauchy_zero  :
0⟩ = 0
theorem real.of_cauchy_one  :
1⟩ = 1
theorem real.of_cauchy_add (a b : cau_seq.completion.Cauchy) :
a + b = a⟩ + b⟩
theorem real.of_cauchy_neg (a : cau_seq.completion.Cauchy) :
-a⟩ = -a⟩
theorem real.of_cauchy_mul (a b : cau_seq.completion.Cauchy) :
a * b = a⟩ * b⟩
theorem real.cauchy_zero  :
0.cauchy = 0
theorem real.cauchy_one  :
1.cauchy = 1
theorem real.cauchy_add (a b : ) :
(a + b).cauchy = a.cauchy + b.cauchy
theorem real.cauchy_neg (a : ) :
theorem real.cauchy_mul (a b : ) :
(a * b).cauchy = a.cauchy * b.cauchy
@[protected, instance]
Equations

Extra instances to short-circuit type class resolution.

These short-circuits have an additional property of ensuring that a computable path is found; if field is found first, then decaying it to these typeclasses would result in a noncomputable version of them.

@[protected, instance]
def real.ring  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations

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

Equations
@[protected, instance]
Equations
theorem real.lt_cauchy {f g : cau_seq has_abs.abs} :
f< g f < g
@[simp]
theorem real.mk_lt {f g : cau_seq has_abs.abs} :
theorem real.mk_zero  :
theorem real.mk_one  :
@[simp]
theorem real.mk_pos {f : cau_seq has_abs.abs} :
@[protected, instance]
Equations
@[simp]
theorem real.mk_le {f g : cau_seq has_abs.abs} :
@[protected]
theorem real.ind_mk {C : → Prop} (x : ) (h : ∀ (y : cau_seq has_abs.abs), C (real.mk y)) :
C x
theorem real.add_lt_add_iff_left {a b : } (c : ) :
c + a < c + b a < b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem real.zero_lt_one  :
0 < 1
@[protected]
theorem real.mul_pos {a b : } :
0 < a0 < b0 < a * b
@[protected, instance]
@[protected, instance]
noncomputable def real.linear_order  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
noncomputable def real.has_inv  :
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def real.field  :
Equations
@[protected, instance]
noncomputable def real.division_ring  :
Equations
@[protected, instance]
noncomputable def real.lattice  :
Equations
@[protected, instance]
noncomputable def real.semilattice_inf  :
Equations
@[protected, instance]
noncomputable def real.semilattice_sup  :
Equations
@[protected, instance]
noncomputable def real.has_inf  :
Equations
@[protected, instance]
noncomputable def real.has_sup  :
Equations
@[protected, instance]
noncomputable def real.decidable_lt (a b : ) :
decidable (a < b)
Equations
@[protected, instance]
noncomputable def real.decidable_le (a b : ) :
Equations
@[protected, instance]
noncomputable def real.decidable_eq (a b : ) :
decidable (a = b)
Equations
@[simp]
theorem real.le_mk_of_forall_le {x : } {f : cau_seq has_abs.abs} :
(∃ (i : ), ∀ (j : ), j ix (f j))x real.mk f
theorem real.mk_le_of_forall_le {f : cau_seq has_abs.abs} {x : } (h : ∃ (i : ), ∀ (j : ), j i(f j) x) :
theorem real.mk_near_of_forall_near {f : cau_seq has_abs.abs} {x ε : } (H : ∃ (i : ), ∀ (j : ), j i|(f j) - x| ε) :
|real.mk f - x| ε
@[protected, instance]
@[protected, instance]
noncomputable def real.floor_ring  :
Equations
theorem real.of_near (f : ) (x : ) (h : ∀ (ε : ), ε > 0(∃ (i : ), ∀ (j : ), j i|(f j) - x| < ε)) :
∃ (h' : is_cau_seq has_abs.abs f), real.mk f, h'⟩ = x
theorem real.exists_floor (x : ) :
∃ (ub : ), ub x ∀ (z : ), z xz ub
theorem real.exists_is_lub (S : set ) (hne : S.nonempty) (hbdd : bdd_above S) :
∃ (x : ), is_lub S x
@[protected, instance]
noncomputable def real.has_Sup  :
Equations
theorem real.Sup_def (S : set ) :
@[protected]
theorem real.is_lub_Sup (S : set ) (h₁ : S.nonempty) (h₂ : bdd_above S) :
@[protected, instance]
noncomputable def real.has_Inf  :
Equations
@[protected]
theorem real.is_glb_Inf (S : set ) (h₁ : S.nonempty) (h₂ : bdd_below S) :
@[protected, instance]
Equations
theorem real.lt_Inf_add_pos {s : set } (h : s.nonempty) {ε : } (hε : 0 < ε) :
∃ (a : ) (H : a s), a < has_Inf.Inf s + ε
theorem real.add_neg_lt_Sup {s : set } (h : s.nonempty) {ε : } (hε : ε < 0) :
∃ (a : ) (H : a s), has_Sup.Sup s + ε < a
theorem real.Inf_le_iff {s : set } (h : bdd_below s) (h' : s.nonempty) {a : } :
has_Inf.Inf s a ∀ (ε : ), 0 < ε(∃ (x : ) (H : x s), x < a + ε)
theorem real.le_Sup_iff {s : set } (h : bdd_above s) (h' : s.nonempty) {a : } :
a has_Sup.Sup s ∀ (ε : ), ε < 0(∃ (x : ) (H : x s), a + ε < x)
@[simp]
theorem real.csupr_empty {α : Sort u_1} [is_empty α] (f : α → ) :
(⨆ (i : α), f i) = 0
@[simp]
theorem real.csupr_const_zero {α : Sort u_1} :
(⨆ (i : α), 0) = 0
theorem real.supr_of_not_bdd_above {α : Sort u_1} {f : α → } (hf : ¬bdd_above (set.range f)) :
(⨆ (i : α), f i) = 0
@[simp]
theorem real.cinfi_empty {α : Sort u_1} [is_empty α] (f : α → ) :
(⨅ (i : α), f i) = 0
@[simp]
theorem real.cinfi_const_zero {α : Sort u_1} :
(⨅ (i : α), 0) = 0
theorem real.infi_of_not_bdd_below {α : Sort u_1} {f : α → } (hf : ¬bdd_below (set.range f)) :
(⨅ (i : α), f i) = 0
theorem real.Sup_nonneg (S : set ) (hS : ∀ (x : ), x S0 x) :

As 0 is the default value for real.Sup of the empty set or sets which are not bounded above, it suffices to show that S is bounded below by 0 to show that 0 ≤ Inf S.

theorem real.Sup_nonpos (S : set ) (hS : ∀ (x : ), x Sx 0) :

As 0 is the default value for real.Sup of the empty set, it suffices to show that S is bounded above by 0 to show that Sup S ≤ 0.

theorem real.Inf_nonneg (S : set ) (hS : ∀ (x : ), x S0 x) :

As 0 is the default value for real.Inf of the empty set, it suffices to show that S is bounded below by 0 to show that 0 ≤ Inf S.

theorem real.Inf_nonpos (S : set ) (hS : ∀ (x : ), x Sx 0) :

As 0 is the default value for real.Inf of the empty set or sets which are not bounded below, it suffices to show that S is bounded above by 0 to show that Inf S ≤ 0.

theorem real.Inf_le_Sup (s : set ) (h₁ : bdd_below s) (h₂ : bdd_above s) :