mathlib documentation

data.real.basic

source
def real  :
Type

Equations
source
def real.comm_ring_aux  :
comm_ring ℝ

Equations
source
@[instance]
def real.comm_ring  :
comm_ring ℝ

Equations
source
@[instance]
def real.ring  :
ring ℝ

Equations
source
@[instance]
def real.comm_semiring  :
comm_semiring ℝ

Equations
source
@[instance]
def real.semiring  :
semiring ℝ

Equations
source
@[instance]
def real.add_comm_group  :
add_comm_group ℝ

Equations
source
@[instance]
def real.add_group  :
add_group ℝ

Equations
source
@[instance]
def real.add_comm_monoid  :
add_comm_monoid ℝ

Equations
source
@[instance]
def real.add_monoid  :
add_monoid ℝ

Equations
source
@[instance]
def real.add_left_cancel_semigroup  :
add_left_cancel_semigroup ℝ

Equations
source
@[instance]
def real.add_right_cancel_semigroup  :
add_right_cancel_semigroup ℝ

Equations
source
@[instance]
def real.add_comm_semigroup  :
add_comm_semigroup ℝ

Equations
source
@[instance]
def real.add_semigroup  :
add_semigroup ℝ

Equations
source
@[instance]
def real.comm_monoid  :
comm_monoid ℝ

Equations
source
@[instance]
def real.monoid  :
monoid ℝ

Equations
source
@[instance]
def real.comm_semigroup  :
comm_semigroup ℝ

Equations
source
@[instance]
def real.semigroup  :
semigroup ℝ

Equations
source
@[instance]
def real.inhabited  :
inhabited ℝ

Equations
source
def real.of_rat  :
ℚ →+* ℝ

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

Equations
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.of_rat_sub (x y : ℚ) :
⇑real.of_rat (x - y) = ⇑real.of_rat x - ⇑real.of_rat y

source
@[instance]
def real.has_lt  :
has_lt ℝ

Equations
source
@[simp]
theorem real.mk_lt {f g : cau_seq ℚ abs} :
real.mk f < real.mk g ↔ f < g

source
theorem real.mk_eq {f g : cau_seq ℚ abs} :
real.mk f = real.mk g ↔ f ≈ g

source
theorem real.quotient_mk_eq_mk (f : cau_seq ℚ abs) :
⟦f⟧ = real.mk f

source
theorem real.mk_eq_mk {f : cau_seq ℚ abs} :
cau_seq.completion.mk f = real.mk f

source
@[simp]
theorem real.mk_pos {f : cau_seq ℚ abs} :
0 < real.mk f ↔ f.pos

source
def real.le (x y : ℝ) :
Prop

Equations
source
@[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
theorem real.add_lt_add_iff_left {a b : ℝ} (c : ℝ) :
c + a < c + b ↔ a < b

source
@[instance]
def real.linear_order  :
linear_order ℝ

Equations
source
@[instance]
def real.partial_order  :
partial_order ℝ

Equations
source
@[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
theorem real.zero_lt_one  :
0 < 1

source
theorem real.mul_pos {a b : ℝ} (a_1 : 0 < a) (a_2 : 0 < b) :
0 < a * b

source
@[instance]
def real.linear_ordered_comm_ring  :
linear_ordered_comm_ring ℝ

Equations
source
@[instance]
def real.linear_ordered_ring  :
linear_ordered_ring ℝ

Equations
source
@[instance]
def real.ordered_ring  :
ordered_ring ℝ

Equations
source
@[instance]
def real.linear_ordered_semiring  :
linear_ordered_semiring ℝ

Equations
source
@[instance]
def real.ordered_semiring  :
ordered_semiring ℝ

Equations
source
@[instance]
def real.ordered_add_comm_group  :
ordered_add_comm_group ℝ

Equations
source
@[instance]
def real.ordered_cancel_add_comm_monoid  :
ordered_cancel_add_comm_monoid ℝ

Equations
source
@[instance]
def real.ordered_add_comm_monoid  :
ordered_add_comm_monoid ℝ

Equations
source
@[instance]
def real.domain  :
domain ℝ

Equations
source
@[instance]
def real.has_one  :
has_one ℝ

Equations
source
@[instance]
def real.has_zero  :
has_zero ℝ

Equations
source
@[instance]
def real.has_mul  :
has_mul ℝ

Equations
source
@[instance]
def real.has_add  :
has_add ℝ

Equations
source
@[instance]
def real.has_sub  :
has_sub ℝ

Equations
source
@[instance]
def real.discrete_linear_ordered_field  :
discrete_linear_ordered_field ℝ

Equations
source
@[instance]
def real.linear_ordered_field  :
linear_ordered_field ℝ

Equations
source
@[instance]
def real.decidable_linear_ordered_comm_ring  :
decidable_linear_ordered_comm_ring ℝ

Equations
source
@[instance]
def real.decidable_linear_ordered_semiring  :
decidable_linear_ordered_semiring ℝ

Equations
source
@[instance]
def real.decidable_linear_ordered_add_comm_group  :
decidable_linear_ordered_add_comm_group ℝ

Equations
source
@[instance]
def real.field  :
field ℝ

Equations
source
@[instance]
def real.division_ring  :
division_ring ℝ

Equations
source
@[instance]
def real.integral_domain  :
integral_domain ℝ

Equations
source
@[instance]
def real.nontrivial  :
nontrivial ℝ

source
@[instance]
def real.decidable_linear_order  :
decidable_linear_order ℝ

Equations
source
@[instance]
def real.distrib_lattice  :
distrib_lattice ℝ

Equations
source
@[instance]
def real.lattice  :
lattice ℝ

Equations
source
@[instance]
def real.semilattice_inf  :
semilattice_inf ℝ

Equations
source
@[instance]
def real.semilattice_sup  :
semilattice_sup ℝ

Equations
source
@[instance]
def real.has_inf  :
has_inf ℝ

Equations
source
@[instance]
def real.has_sup  :
has_sup ℝ

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

Equations
source
@[instance]
def real.decidable_le (a b : ℝ) :
decidable (a ≤ b)

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

Equations
source
theorem real.le_of_forall_epsilon_le {a b : ℝ} (h : ∀ (ε : ℝ), 0 < ε → a ≤ b + ε) :
a ≤ b

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} (a : ∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → x ≤ ↑(⇑f j)) :
x ≤ real.mk f

source
theorem real.mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} (a : ∃ (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 → abs (↑(⇑f j) - x) ≤ ε) :
abs (real.mk f - x) ≤ ε

source
@[instance]
def real.archimedean  :
archimedean ℝ

source
@[instance]
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 → abs (↑(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_sup (S : set ℝ) (a : ∃ (x : ℝ), x ∈ S) (a_1 : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) :
∃ (x : ℝ), ∀ (y : ℝ), x ≤ y ↔ ∀ (z : ℝ), z ∈ S → z ≤ y

source
@[instance]
def real.has_Sup  :
has_Sup ℝ

Equations
source
theorem real.Sup_def (S : set ℝ) :
Sup S = dite ((∃ (x : ℝ), x ∈ S) ∧ ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) (λ (h : (∃ (x : ℝ), x ∈ S) ∧ ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x), classical.some _) (λ (h : ¬((∃ (x : ℝ), x ∈ S) ∧ ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x)), 0)

source
theorem real.Sup_le (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) {y : ℝ} :
Sup S ≤ y ↔ ∀ (z : ℝ), z ∈ S → z ≤ y

source
theorem real.lt_Sup (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) {y : ℝ} :
y < Sup S ↔ ∃ (z : ℝ) (H : z ∈ S), y < z

source
theorem real.le_Sup (S : set ℝ) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) {x : ℝ} (xS : x ∈ S) :
x ≤ Sup S

source
theorem real.Sup_le_ub (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) {ub : ℝ} (h₂ : ∀ (y : ℝ), y ∈ S → y ≤ ub) :
Sup S ≤ ub

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

source
@[instance]
def real.has_Inf  :
has_Inf ℝ

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

source
theorem real.le_Inf (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → x ≤ y) {y : ℝ} :
y ≤ Inf S ↔ ∀ (z : ℝ), z ∈ S → y ≤ z

source
theorem real.Inf_lt (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → x ≤ y) {y : ℝ} :
Inf S < y ↔ ∃ (z : ℝ) (H : z ∈ S), z < y

source
theorem real.Inf_le (S : set ℝ) (h₂ : ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → x ≤ y) {x : ℝ} (xS : x ∈ S) :
Inf S ≤ x

source
theorem real.lb_le_Inf (S : set ℝ) (h₁ : ∃ (x : ℝ), x ∈ S) {lb : ℝ} (h₂ : ∀ (y : ℝ), y ∈ S → lb ≤ y) :
lb ≤ Inf S

source
@[instance]
def real.conditionally_complete_linear_order  :
conditionally_complete_linear_order ℝ

Equations
source
theorem real.Sup_empty  :
Sup ∅ = 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
theorem real.Inf_empty  :
Inf ∅ = 0

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

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

source
@[instance]
def real.cau_seq.is_complete  :
cau_seq.is_complete ℝ abs

Equations
source
theorem real.sqrt_exists {x : ℝ} (a : 0 ≤ x) :
∃ (y : ℝ), 0 ≤ y ∧ y * y = x

source
def real.sqrt_aux (f : cau_seq ℚ abs) (a : ℕ) :
ℚ

Equations
source
theorem real.sqrt_aux_nonneg (f : cau_seq ℚ abs) (i : ℕ) :
0 ≤ real.sqrt_aux f i

source
def real.sqrt (x : ℝ) :
ℝ

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

Equations
source
theorem real.sqrt_prop (x : ℝ) :
0 ≤ real.sqrt x ∧ (real.sqrt x) * real.sqrt x = max 0 x

source
theorem real.sqrt_eq_zero_of_nonpos {x : ℝ} (h : x ≤ 0) :
real.sqrt x = 0

source
theorem real.sqrt_nonneg (x : ℝ) :
0 ≤ real.sqrt x

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

source
@[simp]
theorem real.sqrt_mul_self {x : ℝ} (h : 0 ≤ x) :
real.sqrt (x * x) = x

source
theorem real.sqrt_eq_iff_mul_self_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
real.sqrt x = y ↔ y * y = x

source
@[simp]
theorem real.sqr_sqrt {x : ℝ} (h : 0 ≤ x) :
real.sqrt x ^ 2 = x

source
@[simp]
theorem real.sqrt_sqr {x : ℝ} (h : 0 ≤ x) :
real.sqrt (x ^ 2) = x

source
theorem real.sqrt_eq_iff_sqr_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
real.sqrt x = y ↔ y ^ 2 = x

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

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

source
@[simp]
theorem real.sqrt_zero  :
real.sqrt 0 = 0

source
@[simp]
theorem real.sqrt_one  :
real.sqrt 1 = 1

source
@[simp]
theorem real.sqrt_le {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
real.sqrt x ≤ real.sqrt y ↔ x ≤ y

source
@[simp]
theorem real.sqrt_lt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
real.sqrt x < real.sqrt y ↔ x < y

source
theorem real.sqrt_le_sqrt {x y : ℝ} (h : x ≤ y) :
real.sqrt x ≤ real.sqrt y

source
theorem real.sqrt_le_left {x y : ℝ} (hy : 0 ≤ y) :
real.sqrt x ≤ y ↔ x ≤ y ^ 2

source
theorem real.le_sqrt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
x ≤ real.sqrt y ↔ x ^ 2 ≤ y

source
theorem real.le_sqrt' {x y : ℝ} (hx : 0 < x) :
x ≤ real.sqrt y ↔ x ^ 2 ≤ y

source
theorem real.le_sqrt_of_sqr_le {x y : ℝ} (h : x ^ 2 ≤ y) :
x ≤ real.sqrt y

source
@[simp]
theorem real.sqrt_inj {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
real.sqrt x = real.sqrt y ↔ x = y

source
@[simp]
theorem real.sqrt_eq_zero {x : ℝ} (h : 0 ≤ x) :
real.sqrt x = 0 ↔ x = 0

source
theorem real.sqrt_eq_zero' {x : ℝ} :
real.sqrt x = 0 ↔ x ≤ 0

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

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

source
@[simp]
theorem real.sqrt_mul {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
real.sqrt (x * y) = (real.sqrt x) * real.sqrt y

source
@[simp]
theorem real.sqrt_inv (x : ℝ) :
real.sqrt x⁻¹ = (real.sqrt x)⁻¹

source
@[simp]
theorem real.sqrt_div {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
real.sqrt (x / y) = real.sqrt x / real.sqrt y