mathlib docs: data.real.basic

real.linear_order = {le := has_le.le real.has_le, lt := has_lt.lt real.has_lt, le_refl := real.linear_order._proof_1, le_trans := real.linear_order._proof_2, lt_iff_le_not_le := real.linear_order._proof_3, le_antisymm := real.linear_order._proof_4, le_total := real.linear_order._proof_5}

source

@[instance]

def real.partial_order :

partial_order ℝ

Equations

real.partial_order = linear_order.to_partial_order ℝ

source

@[instance]

def real.preorder :

preorder ℝ

Equations

real.preorder = directed_order.to_preorder

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 : ℝ} :

0 < a → 0 < b → 0 < a * b

source

@[instance]

def real.linear_ordered_comm_ring :

linear_ordered_comm_ring ℝ

Equations

real.linear_ordered_comm_ring = {add := comm_ring.add real.comm_ring, add_assoc := _, zero := comm_ring.zero real.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg real.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul real.comm_ring, mul_assoc := _, one := comm_ring.one real.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_order.le real.linear_order, lt := linear_order.lt real.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := real.linear_ordered_comm_ring._proof_1, exists_pair_ne := real.linear_ordered_comm_ring._proof_2, mul_pos := real.mul_pos, le_total := _, zero_lt_one := real.zero_lt_one, mul_comm := _}

source

@[instance]

def real.linear_ordered_ring :

linear_ordered_ring ℝ

Equations

real.linear_ordered_ring = linear_ordered_comm_ring.to_linear_ordered_ring ℝ

source

@[instance]

def real.ordered_ring :

ordered_ring ℝ

Equations

real.ordered_ring = linear_ordered_ring.to_ordered_ring ℝ

source

@[instance]

def real.linear_ordered_semiring :

linear_ordered_semiring ℝ

Equations

real.linear_ordered_semiring = linear_ordered_ring.to_linear_ordered_semiring

source

@[instance]

def real.ordered_semiring :

ordered_semiring ℝ

Equations

real.ordered_semiring = ordered_ring.to_ordered_semiring

source

@[instance]

def real.ordered_add_comm_group :

ordered_add_comm_group ℝ

Equations

real.ordered_add_comm_group = ordered_ring.to_ordered_add_comm_group ℝ

source

@[instance]

def real.ordered_cancel_add_comm_monoid :

ordered_cancel_add_comm_monoid ℝ

Equations

real.ordered_cancel_add_comm_monoid = ordered_semiring.to_ordered_cancel_add_comm_monoid ℝ

source

@[instance]

def real.ordered_add_comm_monoid :

ordered_add_comm_monoid ℝ

Equations

real.ordered_add_comm_monoid = ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid

source

@[instance]

def real.domain :

domain ℝ

Equations

real.domain = linear_ordered_ring.to_domain

source

@[instance]

def real.has_one :

has_one ℝ

Equations

real.has_one = monoid.to_has_one ℝ

source

@[instance]

def real.has_zero :

has_zero ℝ

Equations

real.has_zero = mul_zero_class.to_has_zero ℝ

source

@[instance]

def real.has_mul :

has_mul ℝ

Equations

real.has_mul = distrib.to_has_mul ℝ

source

@[instance]

def real.has_add :

has_add ℝ

Equations

real.has_add = distrib.to_has_add ℝ

source

@[instance]

def real.has_sub :

has_sub ℝ

Equations

real.has_sub = add_group_has_sub

source

@[instance]

def real.discrete_linear_ordered_field :

discrete_linear_ordered_field ℝ

Equations

real.discrete_linear_ordered_field = {add := linear_ordered_comm_ring.add real.linear_ordered_comm_ring, add_assoc := _, zero := linear_ordered_comm_ring.zero real.linear_ordered_comm_ring, zero_add := _, add_zero := _, neg := linear_ordered_comm_ring.neg real.linear_ordered_comm_ring, add_left_neg := _, add_comm := _, mul := linear_ordered_comm_ring.mul real.linear_ordered_comm_ring, mul_assoc := _, one := linear_ordered_comm_ring.one real.linear_ordered_comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_comm_ring.le real.linear_ordered_comm_ring, lt := linear_ordered_comm_ring.lt real.linear_ordered_comm_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, mul_pos := _, le_total := _, zero_lt_one := _, mul_comm := _, inv := field.inv cau_seq.completion.field, mul_inv_cancel := real.discrete_linear_ordered_field._proof_1, inv_zero := real.discrete_linear_ordered_field._proof_2, decidable_le := λ (a b : ℝ), classical.prop_decidable (a ≤ b), decidable_eq := decidable_linear_ordered_comm_ring.decidable_eq._default linear_ordered_comm_ring.le linear_ordered_comm_ring.lt linear_ordered_comm_ring.le_refl linear_ordered_comm_ring.le_trans linear_ordered_comm_ring.lt_iff_le_not_le linear_ordered_comm_ring.le_antisymm linear_ordered_comm_ring.le_total (λ (a b : ℝ), classical.prop_decidable (a ≤ b)), decidable_lt := decidable_linear_ordered_comm_ring.decidable_lt._default linear_ordered_comm_ring.le linear_ordered_comm_ring.lt linear_ordered_comm_ring.le_refl linear_ordered_comm_ring.le_trans linear_ordered_comm_ring.lt_iff_le_not_le linear_ordered_comm_ring.le_antisymm linear_ordered_comm_ring.le_total (λ (a b : ℝ), classical.prop_decidable (a ≤ b))}

source

@[instance]

def real.linear_ordered_field :

linear_ordered_field ℝ

Equations

real.linear_ordered_field = discrete_linear_ordered_field.to_linear_ordered_field ℝ

source

@[instance]

def real.decidable_linear_ordered_comm_ring :

decidable_linear_ordered_comm_ring ℝ

Equations

real.decidable_linear_ordered_comm_ring = discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ℝ

source

@[instance]

def real.decidable_linear_ordered_semiring :

decidable_linear_ordered_semiring ℝ

Equations

real.decidable_linear_ordered_semiring = decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring

source

@[instance]

def real.decidable_linear_ordered_add_comm_group :

decidable_linear_ordered_add_comm_group ℝ

Equations

real.decidable_linear_ordered_add_comm_group = decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_add_comm_group ℝ

source

@[instance]

def real.field :

field ℝ

Equations

real.field = linear_ordered_field.to_field ℝ

source

@[instance]

def real.division_ring :

division_ring ℝ

Equations

real.division_ring = field.to_division_ring

source

@[instance]

def real.integral_domain :

integral_domain ℝ

Equations

real.integral_domain = field.to_integral_domain

source

@[instance]

def real.nontrivial :

nontrivial ℝ

Equations

real.nontrivial = _

source

@[instance]

def real.decidable_linear_order :

decidable_linear_order ℝ

Equations

real.decidable_linear_order = decidable_linear_ordered_semiring.to_decidable_linear_order ℝ

source

@[instance]

def real.distrib_lattice :

distrib_lattice ℝ

Equations

real.distrib_lattice = distrib_lattice_of_decidable_linear_order

source

@[instance]

def real.lattice :

lattice ℝ

Equations

real.lattice = lattice_of_decidable_linear_order

source

@[instance]

def real.semilattice_inf :

semilattice_inf ℝ

Equations

real.semilattice_inf = lattice.to_semilattice_inf ℝ

source

@[instance]

def real.semilattice_sup :

semilattice_sup ℝ

Equations

real.semilattice_sup = lattice.to_semilattice_sup ℝ

source

@[instance]

def real.has_inf :

has_inf ℝ

Equations

real.has_inf = semilattice_inf.to_has_inf ℝ

source

@[instance]

def real.has_sup :

has_sup ℝ

Equations

real.has_sup = semilattice_sup.to_has_sup ℝ

source

@[instance]

def real.decidable_lt (a b : ℝ) :

decidable (a < b)

Equations

a.decidable_lt b = has_lt.lt.decidable a b

source

@[instance]

def real.decidable_le (a b : ℝ) :

decidable (a ≤ b)

Equations

a.decidable_le b = has_le.le.decidable a b

source

@[instance]

def real.decidable_eq (a b : ℝ) :

decidable (a = b)

Equations

a.decidable_eq b = quotient.decidable_eq a b

source

theorem real.le_of_forall_epsilon_le {a b : ℝ} :

(∀ (ε : ℝ), 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} :

(∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → x ≤ ↑(⇑f j)) → x ≤ real.mk f

source

theorem real.mk_le_of_forall_le {f : cau_seq ℚ abs} {x : ℝ} :

(∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → ↑(⇑f j) ≤ x) → real.mk f ≤ x

source

theorem real.mk_near_of_forall_near {f : cau_seq ℚ abs} {x ε : ℝ} :

(∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → abs (↑(⇑f j) - x) ≤ ε) → abs (real.mk f - x) ≤ ε

source

@[instance]

def real.archimedean :

archimedean ℝ

Equations

real.archimedean = _
_ = _

source

@[instance]

def real.floor_ring :

floor_ring ℝ

Equations

real.floor_ring = archimedean.floor_ring ℝ

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 : ℝ) :

(∀ (ε : ℝ), ε > 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 ℝ) :

(∃ (x : ℝ), x ∈ S) → (∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x) → (∃ (x : ℝ), ∀ (y : ℝ), x ≤ y ↔ ∀ (z : ℝ), z ∈ S → z ≤ y)

source

@[instance]

def real.has_Sup :

has_Sup ℝ

Equations

real.has_Sup = {Sup := λ (S : set ℝ), 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_def (S : set ℝ) :

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