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 ℚ.

source
structure real  :
Type

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

source
theorem real.ext_cauchy_iff {x y : ℝ} :
x = y ↔ x.cauchy = y.cauchy
source
theorem real.ext_cauchy {x y : ℝ} :
x.cauchy = y.cauchy → x = y
source
def real.equiv_Cauchy  :
ℝ ≃ cau_seq.completion.Cauchy

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

Equations
source
@[protected, instance]
def real.has_zero  :
has_zero ℝ
Equations
source
@[protected, instance]
def real.has_one  :
has_one ℝ
Equations
source
@[protected, instance]
def real.has_add  :
has_add ℝ
Equations
source
@[protected, instance]
def real.has_neg  :
has_neg ℝ
Equations
source
@[protected, instance]
def real.has_mul  :
has_mul ℝ
Equations
source
theorem real.of_cauchy_zero  :
⟨0⟩ = 0
source
theorem real.of_cauchy_one  :
⟨1⟩ = 1
source
theorem real.of_cauchy_add (a b : cau_seq.completion.Cauchy) :
⟨a + b⟩ = ⟨a⟩ + ⟨b⟩
source
theorem real.of_cauchy_neg (a : cau_seq.completion.Cauchy) :
⟨-a⟩ = -⟨a⟩
source
theorem real.of_cauchy_mul (a b : cau_seq.completion.Cauchy) :
⟨a * b⟩ = ⟨a⟩ * ⟨b⟩
source
theorem real.cauchy_zero  :
0.cauchy = 0
source
theorem real.cauchy_one  :
1.cauchy = 1
source
theorem real.cauchy_add (a b : ℝ) :
(a + b).cauchy = a.cauchy + b.cauchy
source
theorem real.cauchy_neg (a : ℝ) :
(-a).cauchy = -a.cauchy
source
theorem real.cauchy_mul (a b : ℝ) :
(a * b).cauchy = (a.cauchy) * b.cauchy
source
@[protected, instance]
def real.comm_ring  :
comm_ring ℝ
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.

source
@[protected, instance]
def real.ring  :
ring ℝ
Equations
source
@[protected, instance]
def real.comm_semiring  :
comm_semiring ℝ
Equations
source
@[protected, instance]
def real.semiring  :
semiring ℝ
Equations
source
@[protected, instance]
def real.comm_monoid_with_zero  :
comm_monoid_with_zero ℝ
Equations
source
@[protected, instance]
def real.monoid_with_zero  :
monoid_with_zero ℝ
Equations
source
@[protected, instance]
def real.add_comm_group  :
add_comm_group ℝ
Equations
source
@[protected, instance]
def real.add_group  :
add_group ℝ
Equations
source
@[protected, instance]
def real.add_comm_monoid  :
add_comm_monoid ℝ
Equations
source
@[protected, instance]
def real.add_monoid  :
add_monoid ℝ
Equations
source
@[protected, instance]
def real.add_left_cancel_semigroup  :
add_left_cancel_semigroup ℝ
Equations
source
@[protected, instance]
def real.add_right_cancel_semigroup  :
add_right_cancel_semigroup ℝ
Equations
source
@[protected, instance]
def real.add_comm_semigroup  :
add_comm_semigroup ℝ
Equations
source
@[protected, instance]
def real.add_semigroup  :
add_semigroup ℝ
Equations
source
@[protected, instance]
def real.comm_monoid  :
comm_monoid ℝ
Equations
source
@[protected, instance]
def real.monoid  :
monoid ℝ
Equations
source
@[protected, instance]
def real.comm_semigroup  :
comm_semigroup ℝ
Equations
source
@[protected, instance]
def real.semigroup  :
semigroup ℝ
Equations
source
@[protected, instance]
def real.has_sub  :
has_sub ℝ
Equations
source
@[protected, instance]
def real.module  :
module ℝ ℝ
Equations
source
@[protected, instance]
def real.inhabited  :
inhabited ℝ
Equations
source
@[protected, instance]
def real.star_ring  :
star_ring ℝ

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

Equations
source
@[protected, instance]
def real.has_trivial_star  :
has_trivial_star ℝ
source
def real.of_rat  :
ℚ →+* ℝ

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

Equations
source
theorem real.of_rat_apply (x : ℚ) :
⇑real.of_rat x = ⟨cau_seq.completion.of_rat x⟩
source
def real.mk (x : cau_seq ℚ abs) :
ℝ

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

Equations
source
theorem real.mk_eq {f g : cau_seq ℚ abs} :
real.mk f = real.mk g ↔ f ≈ g
source
@[protected, instance]
def real.has_lt  :
has_lt ℝ
Equations
source
theorem real.lt_cauchy {f g : cau_seq ℚ abs} :
⟨⟦f⟧⟩ < ⟨⟦g⟧⟩ ↔ f < g
source
@[simp]
theorem real.mk_lt {f g : cau_seq ℚ abs} :
real.mk f < real.mk g ↔ f < g
source
theorem real.mk_zero  :
real.mk 0 = 0
source
theorem real.mk_one  :
real.mk 1 = 1
source
theorem real.mk_add {f g : cau_seq ℚ abs} :
real.mk (f + g) = real.mk f + real.mk g
source
theorem real.mk_mul {f g : cau_seq ℚ abs} :
real.mk (f * g) = (real.mk f) * real.mk g
source
theorem real.mk_neg {f : cau_seq ℚ abs} :
real.mk (-f) = -real.mk f
source
@[simp]
theorem real.mk_pos {f : cau_seq ℚ abs} :
0 < real.mk f ↔ f.pos
source
@[protected, instance]
def real.has_le  :
has_le ℝ
Equations
source
@[simp]
theorem real.mk_le {f g : cau_seq ℚ abs} :
real.mk f ≤ real.mk g ↔ f ≤ g
source
@[protected]
theorem real.ind_mk {C : ℝ → Prop} (x : ℝ) (h : ∀ (y : cau_seq ℚ abs), C (real.mk y)) :
C x
source
theorem real.add_lt_add_iff_left {a b : ℝ} (c : ℝ) :
c + a < c + b ↔ a < b
source
@[protected, instance]
def real.partial_order  :
partial_order ℝ
Equations
source
@[protected, instance]
def real.preorder  :
preorder ℝ
Equations
source
theorem real.of_rat_lt {x y : ℚ} :
⇑real.of_rat x < ⇑real.of_rat y ↔ x < y
source
@[protected]
theorem real.zero_lt_one  :
0 < 1
source
@[protected]
theorem real.mul_pos {a b : ℝ} :
0 < a → 0 < b → 0 < a * b
source
@[protected, instance]
def real.ordered_comm_ring  :
ordered_comm_ring ℝ
Equations
source
@[protected, instance]
def real.ordered_ring  :
ordered_ring ℝ
Equations
source
@[protected, instance]
def real.ordered_semiring  :
ordered_semiring ℝ
Equations
source
@[protected, instance]
def real.ordered_add_comm_group  :
ordered_add_comm_group ℝ
Equations
source
@[protected, instance]
def real.ordered_cancel_add_comm_monoid  :
ordered_cancel_add_comm_monoid ℝ
Equations
source
@[protected, instance]
def real.ordered_add_comm_monoid  :
ordered_add_comm_monoid ℝ
Equations
source
@[protected, instance]
def real.nontrivial  :
nontrivial ℝ
source
@[protected, instance]
noncomputable def real.linear_order  :
linear_order ℝ
Equations
source
@[protected, instance]
noncomputable def real.linear_ordered_comm_ring  :
linear_ordered_comm_ring ℝ
Equations
source
@[protected, instance]
noncomputable def real.linear_ordered_ring  :
linear_ordered_ring ℝ
Equations
source
@[protected, instance]
noncomputable def real.linear_ordered_semiring  :
linear_ordered_semiring ℝ
Equations
source
@[protected, instance]
def real.is_domain  :
is_domain ℝ
source
@[protected, instance]
noncomputable def real.has_inv  :
has_inv ℝ
Equations
source
theorem real.of_cauchy_inv {f : cau_seq.completion.Cauchy} :
⟨f⁻¹⟩ = ⟨f⟩⁻¹
source
theorem real.cauchy_inv (f : ℝ) :
f⁻¹.cauchy = (f.cauchy)⁻¹
source
@[protected, instance]
noncomputable def real.linear_ordered_field  :
linear_ordered_field ℝ
Equations
source
@[protected, instance]
noncomputable def real.linear_ordered_add_comm_group  :
linear_ordered_add_comm_group ℝ
Equations
source
@[protected, instance]
noncomputable def real.field  :
field ℝ
Equations
source
@[protected, instance]
noncomputable def real.division_ring  :
division_ring ℝ
Equations
source
@[protected, instance]
noncomputable def real.distrib_lattice  :
distrib_lattice ℝ
Equations
source
@[protected, instance]
noncomputable def real.lattice  :
lattice ℝ
Equations
source
@[protected, instance]
noncomputable def real.semilattice_inf  :
semilattice_inf ℝ
Equations
source
@[protected, instance]
noncomputable def real.semilattice_sup  :
semilattice_sup ℝ
Equations
source
@[protected, instance]
noncomputable def real.has_inf  :
has_inf ℝ
Equations
source
@[protected, instance]
noncomputable def real.has_sup  :
has_sup ℝ
Equations
source
@[protected, instance]
noncomputable def real.decidable_lt (a b : ℝ) :
decidable (a < b)
Equations
source
@[protected, instance]
noncomputable def real.decidable_le (a b : ℝ) :
decidable (a ≤ b)
Equations
source
@[protected, instance]
noncomputable def real.decidable_eq (a b : ℝ) :
decidable (a = b)
Equations
source
@[simp]
theorem real.of_rat_eq_cast (x : ℚ) :
⇑real.of_rat x = ↑x
source
theorem real.le_mk_of_forall_le {x : ℝ} {f : cau_seq ℚ abs} :
(∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → x ≤ ↑(⇑f j)) → x ≤ real.mk f
source
theorem real.mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} (h : ∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → ↑(⇑f j) ≤ x) :
real.mk f ≤ x
source
theorem real.mk_near_of_forall_near {f : cau_seq ℚ abs} {x ε : ℝ} (H : ∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → |↑(⇑f j) - x| ≤ ε) :
|real.mk f - x| ≤ ε
source
@[protected, instance]
def real.archimedean  :
archimedean ℝ
source
@[protected, instance]
noncomputable def real.floor_ring  :
floor_ring ℝ
Equations
source
theorem real.is_cau_seq_iff_lift {f : ℕ → ℚ} :
is_cau_seq abs f ↔ is_cau_seq abs (λ (i : ℕ), ↑(f i))
source
theorem real.of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ (ε : ℝ), ε > 0 → (∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → |↑(f j) - x| < ε)) :
∃ (h' : is_cau_seq abs f), real.mk ⟨f, h'⟩ = x
source
theorem real.exists_floor (x : ℝ) :
∃ (ub : ℤ), ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
source
theorem real.exists_is_lub (S : set ℝ) (hne : S.nonempty) (hbdd : bdd_above S) :
∃ (x : ℝ), is_lub S x
source
@[protected, instance]
noncomputable def real.has_Sup  :
has_Sup ℝ
Equations
source
theorem real.Sup_def (S : set ℝ) :
Sup S = dite (S.nonempty ∧ bdd_above S) (λ (h : S.nonempty ∧ bdd_above S), classical.some _) (λ (h : ¬(S.nonempty ∧ bdd_above S)), 0)
source
@[protected]
theorem real.is_lub_Sup (S : set ℝ) (h₁ : S.nonempty) (h₂ : bdd_above S) :
is_lub S (Sup S)
source
@[protected, instance]
noncomputable def real.has_Inf  :
has_Inf ℝ
Equations
source
theorem real.Inf_def (S : set ℝ) :
Inf S = -Sup (-S)
source
@[protected]
theorem real.is_glb_Inf (S : set ℝ) (h₁ : S.nonempty) (h₂ : bdd_below S) :
is_glb S (Inf S)
source
@[protected, instance]
noncomputable def real.conditionally_complete_linear_order  :
conditionally_complete_linear_order ℝ
Equations
source
theorem real.lt_Inf_add_pos {s : set ℝ} (h : s.nonempty) {ε : ℝ} (hε : 0 < ε) :
∃ (a : ℝ) (H : a ∈ s), a < Inf s + ε
source
theorem real.add_neg_lt_Sup {s : set ℝ} (h : s.nonempty) {ε : ℝ} (hε : ε < 0) :
∃ (a : ℝ) (H : a ∈ s), Sup s + ε < a
source
theorem real.Inf_le_iff {s : set ℝ} (h : bdd_below s) (h' : s.nonempty) {a : ℝ} :
Inf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → (∃ (x : ℝ) (H : x ∈ s), x < a + ε)
source
theorem real.le_Sup_iff {s : set ℝ} (h : bdd_above s) (h' : s.nonempty) {a : ℝ} :
a ≤ Sup s ↔ ∀ (ε : ℝ), ε < 0 → (∃ (x : ℝ) (H : x ∈ s), a + ε < x)
source
@[simp]
theorem real.Sup_empty  :
Sup ∅ = 0
source
theorem real.csupr_empty {α : Sort u_1} [is_empty α] (f : α → ℝ) :
(⨆ (i : α), f i) = 0
source
@[simp]
theorem real.csupr_const_zero {α : Sort u_1} :
(⨆ (i : α), 0) = 0
source
theorem real.Sup_of_not_bdd_above {s : set ℝ} (hs : ¬bdd_above s) :
Sup s = 0
source
theorem real.Sup_univ  :
Sup set.univ = 0
source
@[simp]
theorem real.Inf_empty  :
Inf ∅ = 0
source
theorem real.cinfi_empty {α : Sort u_1} [is_empty α] (f : α → ℝ) :
(⨅ (i : α), f i) = 0
source
@[simp]
theorem real.cinfi_const_zero {α : Sort u_1} :
(⨅ (i : α), 0) = 0
source
theorem real.Inf_of_not_bdd_below {s : set ℝ} (hs : ¬bdd_below s) :
Inf s = 0
source
theorem real.Sup_nonneg (S : set ℝ) (hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x) :
0 ≤ Sup S

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.

source
theorem real.Sup_nonpos (S : set ℝ) (hS : ∀ (x : ℝ), x ∈ S → x ≤ 0) :
Sup S ≤ 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.

source
theorem real.Inf_nonneg (S : set ℝ) (hS : ∀ (x : ℝ), x ∈ S → 0 ≤ x) :
0 ≤ Inf S

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.

source
theorem real.Inf_nonpos (S : set ℝ) (hS : ∀ (x : ℝ), x ∈ S → x ≤ 0) :
Inf S ≤ 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.

source
theorem real.Inf_le_Sup (s : set ℝ) (h₁ : bdd_below s) (h₂ : bdd_above s) :
Inf s ≤ Sup s
source
theorem real.cau_seq_converges (f : cau_seq ℝ abs) :
∃ (x : ℝ), f ≈ cau_seq.const abs x
source
@[protected, instance]
def real.has_abs.abs.cau_seq.is_complete  :
cau_seq.is_complete ℝ abs