data.real.basic - mathlib3 docs

real.equiv_Cauchy = {to_fun := real.cauchy, inv_fun := real.of_cauchy, left_inv := real.equiv_Cauchy._proof_1, right_inv := real.equiv_Cauchy._proof_2}

source

@[protected, instance]

def real.has_zero :

has_zero ℝ

Equations

real.has_zero = {zero := zero}

source

@[protected, instance]

def real.has_one :

has_one ℝ

Equations

real.has_one = {one := one}

source

@[protected, instance]

def real.has_add :

has_add ℝ

Equations

real.has_add = {add := add}

source

@[protected, instance]

def real.has_neg :

has_neg ℝ

Equations

real.has_neg = {neg := neg}

source

@[protected, instance]

def real.has_mul :

has_mul ℝ

Equations

real.has_mul = {mul := mul}

source

@[protected, instance]

def real.has_sub :

has_sub ℝ

Equations

real.has_sub = {sub := λ (a b : ℝ), a + -b}

source

@[protected, instance]

noncomputable def real.has_inv :

has_inv ℝ

Equations

real.has_inv = {inv := inv'}

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 has_abs.abs) :

⟨a + b⟩ = ⟨a⟩ + ⟨b⟩

source

theorem real.of_cauchy_neg (a : cau_seq.completion.Cauchy has_abs.abs) :

⟨-a⟩ = -⟨a⟩

source

theorem real.of_cauchy_sub (a b : cau_seq.completion.Cauchy has_abs.abs) :

⟨a - b⟩ = ⟨a⟩ - ⟨b⟩

source

theorem real.of_cauchy_mul (a b : cau_seq.completion.Cauchy has_abs.abs) :

⟨a * b⟩ = ⟨a⟩ * ⟨b⟩

source

theorem real.of_cauchy_inv {f : cau_seq.completion.Cauchy has_abs.abs} :

⟨f⁻¹⟩ = ⟨f⟩⁻¹

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

theorem real.cauchy_sub (a b : ℝ) :

(a - b).cauchy = a.cauchy - b.cauchy

source

theorem real.cauchy_inv (f : ℝ) :

f⁻¹.cauchy = (f.cauchy)⁻¹

source

@[protected, instance]

def real.has_nat_cast :

has_nat_cast ℝ

Equations

real.has_nat_cast = {nat_cast := λ (n : ℕ), ⟨↑n⟩}

source

@[protected, instance]

def real.has_int_cast :

has_int_cast ℝ

Equations

real.has_int_cast = {int_cast := λ (z : ℤ), ⟨↑z⟩}

source

@[protected, instance]

def real.has_rat_cast :

has_rat_cast ℝ

Equations

real.has_rat_cast = {rat_cast := λ (q : ℚ), ⟨↑q⟩}

source

theorem real.of_cauchy_nat_cast (n : ℕ) :

⟨↑n⟩ = ↑n

source

theorem real.of_cauchy_int_cast (z : ℤ) :

⟨↑z⟩ = ↑z

source

theorem real.of_cauchy_rat_cast (q : ℚ) :

⟨↑q⟩ = ↑q

source

theorem real.cauchy_nat_cast (n : ℕ) :

↑n.cauchy = ↑n

source

theorem real.cauchy_int_cast (z : ℤ) :

↑z.cauchy = ↑z

source

theorem real.cauchy_rat_cast (q : ℚ) :

↑q.cauchy = ↑q

source

@[protected, instance]

def real.comm_ring :

comm_ring ℝ

Equations

real.comm_ring = {add := has_add.add real.has_add, add_assoc := real.comm_ring._proof_1, zero := 0, zero_add := real.comm_ring._proof_2, add_zero := real.comm_ring._proof_3, nsmul := nsmul_rec {add := has_add.add real.has_add}, nsmul_zero' := real.comm_ring._proof_4, nsmul_succ' := real.comm_ring._proof_5, neg := has_neg.neg real.has_neg, sub := has_sub.sub real.has_sub, sub_eq_add_neg := real.comm_ring._proof_6, zsmul := zsmul_rec {neg := has_neg.neg real.has_neg}, zsmul_zero' := real.comm_ring._proof_7, zsmul_succ' := real.comm_ring._proof_8, zsmul_neg' := real.comm_ring._proof_9, add_left_neg := real.comm_ring._proof_10, add_comm := real.comm_ring._proof_11, int_cast := has_int_cast.int_cast real.has_int_cast, nat_cast := has_nat_cast.nat_cast real.has_nat_cast, one := 1, nat_cast_zero := real.comm_ring._proof_12, nat_cast_succ := real.comm_ring._proof_13, int_cast_of_nat := real.comm_ring._proof_14, int_cast_neg_succ_of_nat := real.comm_ring._proof_15, mul := has_mul.mul real.has_mul, mul_assoc := real.comm_ring._proof_16, one_mul := real.comm_ring._proof_17, mul_one := real.comm_ring._proof_18, npow := npow_rec {mul := has_mul.mul real.has_mul}, npow_zero' := real.comm_ring._proof_19, npow_succ' := real.comm_ring._proof_20, left_distrib := real.comm_ring._proof_21, right_distrib := real.comm_ring._proof_22, mul_comm := real.comm_ring._proof_23}

source

@[simp]

theorem real.ring_equiv_Cauchy_symm_apply_cauchy (cauchy : cau_seq.completion.Cauchy has_abs.abs) :

(⇑(real.ring_equiv_Cauchy.symm) cauchy).cauchy = cauchy

source

@[simp]

theorem real.ring_equiv_Cauchy_apply (self : ℝ) :

⇑real.ring_equiv_Cauchy self = self.cauchy

source

def real.ring_equiv_Cauchy :

ℝ ≃+* cau_seq.completion.Cauchy has_abs.abs

real.equiv_Cauchy as a ring equivalence.

Equations

real.ring_equiv_Cauchy = {to_fun := real.cauchy, inv_fun := real.of_cauchy, left_inv := real.ring_equiv_Cauchy._proof_1, right_inv := real.ring_equiv_Cauchy._proof_2, map_mul' := real.cauchy_mul, map_add' := real.cauchy_add}

source

@[protected, instance]

def real.ring :

ring ℝ

Equations

real.ring = comm_ring.to_ring ℝ

source

@[protected, instance]

def real.comm_semiring :

comm_semiring ℝ

Equations

real.comm_semiring = comm_ring.to_comm_semiring

source

@[protected, instance]

def real.semiring :

semiring ℝ

Equations

real.semiring = ring.to_semiring

source

@[protected, instance]

def real.comm_monoid_with_zero :

comm_monoid_with_zero ℝ

Equations

real.comm_monoid_with_zero = comm_semiring.to_comm_monoid_with_zero

source

@[protected, instance]

def real.monoid_with_zero :

monoid_with_zero ℝ

Equations

real.monoid_with_zero = semiring.to_monoid_with_zero ℝ

source

@[protected, instance]

def real.add_comm_group :

add_comm_group ℝ

Equations

real.add_comm_group = non_unital_non_assoc_ring.to_add_comm_group ℝ

source

@[protected, instance]

def real.add_group :

add_group ℝ

Equations

real.add_group = add_group_with_one.to_add_group ℝ

source

@[protected, instance]

def real.add_comm_monoid :

add_comm_monoid ℝ

Equations

real.add_comm_monoid = add_comm_group.to_add_comm_monoid ℝ

source

@[protected, instance]

def real.add_monoid :

add_monoid ℝ

Equations

real.add_monoid = add_monoid_with_one.to_add_monoid ℝ

source

@[protected, instance]

def real.add_left_cancel_semigroup :

add_left_cancel_semigroup ℝ

Equations

real.add_left_cancel_semigroup = add_left_cancel_monoid.to_add_left_cancel_semigroup ℝ

source

@[protected, instance]

def real.add_right_cancel_semigroup :

add_right_cancel_semigroup ℝ

Equations

real.add_right_cancel_semigroup = add_right_cancel_monoid.to_add_right_cancel_semigroup ℝ

source

@[protected, instance]

def real.add_comm_semigroup :

add_comm_semigroup ℝ

Equations

real.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup ℝ

source

@[protected, instance]

def real.add_semigroup :

add_semigroup ℝ

Equations

real.add_semigroup = add_monoid.to_add_semigroup ℝ

source

@[protected, instance]

def real.comm_monoid :

comm_monoid ℝ

Equations

real.comm_monoid = comm_ring.to_comm_monoid ℝ

source

@[protected, instance]

def real.monoid :

monoid ℝ

Equations

real.monoid = ring.to_monoid ℝ

source

@[protected, instance]

def real.comm_semigroup :

comm_semigroup ℝ

Equations

real.comm_semigroup = non_unital_comm_ring.to_comm_semigroup ℝ

source

@[protected, instance]

def real.semigroup :

semigroup ℝ

Equations

real.semigroup = semigroup_with_zero.to_semigroup ℝ

source

@[protected, instance]

def real.inhabited :

inhabited ℝ

Equations

real.inhabited = {default := 0}

source

@[protected, instance]

def real.star_ring :

star_ring ℝ

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

Equations

real.star_ring = star_ring_of_comm

source

@[protected, instance]

def real.has_trivial_star :

has_trivial_star ℝ

source

def real.mk (x : cau_seq ℚ has_abs.abs) :

ℝ

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

Equations

real.mk x = ⟨cau_seq.completion.mk x⟩

source

theorem real.mk_eq {f g : cau_seq ℚ has_abs.abs} :

real.mk f = real.mk g ↔ f ≈ g

source

@[protected, instance]

def real.has_lt :

has_lt ℝ

Equations

real.has_lt = {lt := lt}

source

theorem real.lt_cauchy {f g : cau_seq ℚ has_abs.abs} :

⟨⟦f⟧⟩ < ⟨⟦g⟧⟩ ↔ f < g

source

@[simp]

theorem real.mk_lt {f g : cau_seq ℚ has_abs.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 ℚ has_abs.abs} :

real.mk (f + g) = real.mk f + real.mk g

source

theorem real.mk_mul {f g : cau_seq ℚ has_abs.abs} :

real.mk (f * g) = real.mk f * real.mk g

source

theorem real.mk_neg {f : cau_seq ℚ has_abs.abs} :

real.mk (-f) = -real.mk f

source

@[simp]

theorem real.mk_pos {f : cau_seq ℚ has_abs.abs} :

0 < real.mk f ↔ f.pos

source

@[protected, instance]

def real.has_le :

has_le ℝ

Equations

real.has_le = {le := le}

source

@[simp]

theorem real.mk_le {f g : cau_seq ℚ has_abs.abs} :

real.mk f ≤ real.mk g ↔ f ≤ g

source

@[protected]

theorem real.ind_mk {C : ℝ → Prop} (x : ℝ) (h : ∀ (y : cau_seq ℚ has_abs.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

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

source

@[protected, instance]

def real.preorder :

preorder ℝ

Equations

real.preorder = partial_order.to_preorder ℝ

source

theorem real.rat_cast_lt {x y : ℚ} :

↑x < ↑y ↔ x < y

source

@[protected]

theorem real.zero_lt_one :

0 < 1

source

@[protected]

theorem real.fact_zero_lt_one :

fact (0 < 1)

source

@[protected]

theorem real.mul_pos {a b : ℝ} :

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

source

@[protected, instance]

def real.strict_ordered_comm_ring :

strict_ordered_comm_ring ℝ

Equations

real.strict_ordered_comm_ring = {add := comm_ring.add real.comm_ring, add_assoc := _, zero := comm_ring.zero real.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul real.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg real.comm_ring, sub := comm_ring.sub real.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul real.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast real.comm_ring, nat_cast := comm_ring.nat_cast real.comm_ring, one := comm_ring.one real.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul real.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow real.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := partial_order.le real.partial_order, lt := partial_order.lt real.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := real.strict_ordered_comm_ring._proof_1, exists_pair_ne := real.strict_ordered_comm_ring._proof_2, zero_le_one := real.strict_ordered_comm_ring._proof_3, mul_pos := real.mul_pos, mul_comm := _}

source

@[protected, instance]

def real.strict_ordered_ring :

strict_ordered_ring ℝ

Equations

real.strict_ordered_ring = infer_instance

source

@[protected, instance]

def real.strict_ordered_comm_semiring :

strict_ordered_comm_semiring ℝ

Equations

real.strict_ordered_comm_semiring = infer_instance

source

@[protected, instance]

def real.strict_ordered_semiring :

strict_ordered_semiring ℝ

Equations

real.strict_ordered_semiring = infer_instance

source

@[protected, instance]

def real.ordered_ring :

ordered_ring ℝ

Equations

real.ordered_ring = infer_instance

source

@[protected, instance]

def real.ordered_semiring :

ordered_semiring ℝ

Equations

real.ordered_semiring = infer_instance

source

@[protected, instance]

def real.ordered_add_comm_group :

ordered_add_comm_group ℝ

Equations

real.ordered_add_comm_group = infer_instance

source

@[protected, instance]

def real.ordered_cancel_add_comm_monoid :

ordered_cancel_add_comm_monoid ℝ

Equations

real.ordered_cancel_add_comm_monoid = infer_instance

source

@[protected, instance]

def real.ordered_add_comm_monoid :

ordered_add_comm_monoid ℝ

Equations

real.ordered_add_comm_monoid = infer_instance

source

@[protected, instance]

def real.nontrivial :

nontrivial ℝ

source

@[protected, instance]

def real.has_sup :

has_sup ℝ

Equations

real.has_sup = {sup := sup}

source

theorem real.of_cauchy_sup (a b : cau_seq ℚ has_abs.abs) :

⟨⟦a ⊔ b⟧⟩ = ⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩

source

@[simp]

theorem real.mk_sup (a b : cau_seq ℚ has_abs.abs) :

real.mk (a ⊔ b) = real.mk a ⊔ real.mk b

source

@[protected, instance]

def real.has_inf :

has_inf ℝ

Equations

real.has_inf = {inf := inf}

source

theorem real.of_cauchy_inf (a b : cau_seq ℚ has_abs.abs) :

⟨⟦a ⊓ b⟧⟩ = ⟨⟦a⟧⟩ ⊓ ⟨⟦b⟧⟩

source

@[simp]

theorem real.mk_inf (a b : cau_seq ℚ has_abs.abs) :

real.mk (a ⊓ b) = real.mk a ⊓ real.mk b

source

@[protected, instance]

def real.distrib_lattice :

distrib_lattice ℝ

Equations

real.distrib_lattice = {sup := has_sup.sup real.has_sup, le := has_le.le real.has_le, lt := partial_order.lt real.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := real.distrib_lattice._proof_1, le_sup_right := real.distrib_lattice._proof_2, sup_le := real.distrib_lattice._proof_3, inf := has_inf.inf real.has_inf, inf_le_left := real.distrib_lattice._proof_4, inf_le_right := real.distrib_lattice._proof_5, le_inf := real.distrib_lattice._proof_6, le_sup_inf := real.distrib_lattice._proof_7}

source

@[protected, instance]

def real.lattice :

lattice ℝ

Equations

real.lattice = infer_instance

source

@[protected, instance]

def real.semilattice_inf :

semilattice_inf ℝ

Equations

real.semilattice_inf = infer_instance

source

@[protected, instance]

def real.semilattice_sup :

semilattice_sup ℝ

Equations

real.semilattice_sup = infer_instance

source

@[protected, instance]

def real.has_le.le.is_total :

is_total ℝ has_le.le

source

@[protected, instance]

noncomputable def real.linear_order :

linear_order ℝ

Equations

real.linear_order = lattice.to_linear_order ℝ

source

@[protected, instance]

noncomputable def real.linear_ordered_comm_ring :

linear_ordered_comm_ring ℝ

Equations

real.linear_ordered_comm_ring = {add := strict_ordered_ring.add real.strict_ordered_ring, add_assoc := _, zero := strict_ordered_ring.zero real.strict_ordered_ring, zero_add := _, add_zero := _, nsmul := strict_ordered_ring.nsmul real.strict_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := strict_ordered_ring.neg real.strict_ordered_ring, sub := strict_ordered_ring.sub real.strict_ordered_ring, sub_eq_add_neg := _, zsmul := strict_ordered_ring.zsmul real.strict_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := strict_ordered_ring.int_cast real.strict_ordered_ring, nat_cast := strict_ordered_ring.nat_cast real.strict_ordered_ring, one := strict_ordered_ring.one real.strict_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := strict_ordered_ring.mul real.strict_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := strict_ordered_ring.npow real.strict_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := strict_ordered_ring.le real.strict_ordered_ring, lt := strict_ordered_ring.lt real.strict_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le real.linear_order, decidable_eq := linear_order.decidable_eq real.linear_order, decidable_lt := linear_order.decidable_lt real.linear_order, max := linear_order.max real.linear_order, max_def := _, min := linear_order.min real.linear_order, min_def := _, mul_comm := _}

source

@[protected, instance]

noncomputable def real.linear_ordered_ring :

linear_ordered_ring ℝ

Equations

real.linear_ordered_ring = linear_ordered_comm_ring.to_linear_ordered_ring ℝ

source

@[protected, instance]

noncomputable def real.linear_ordered_semiring :

linear_ordered_semiring ℝ

Equations

real.linear_ordered_semiring = linear_ordered_ring.to_linear_ordered_semiring

source

@[protected, instance]

def real.is_domain :

is_domain ℝ

source

@[protected, instance]

noncomputable def real.linear_ordered_field :

linear_ordered_field ℝ

Equations

real.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 := _, nsmul := linear_ordered_comm_ring.nsmul real.linear_ordered_comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_comm_ring.neg real.linear_ordered_comm_ring, sub := linear_ordered_comm_ring.sub real.linear_ordered_comm_ring, sub_eq_add_neg := _, zsmul := linear_ordered_comm_ring.zsmul real.linear_ordered_comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_comm_ring.int_cast real.linear_ordered_comm_ring, nat_cast := linear_ordered_comm_ring.nat_cast real.linear_ordered_comm_ring, one := linear_ordered_comm_ring.one real.linear_ordered_comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_comm_ring.mul real.linear_ordered_comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_comm_ring.npow real.linear_ordered_comm_ring, npow_zero' := _, npow_succ' := _, 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 := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_comm_ring.decidable_le real.linear_ordered_comm_ring, decidable_eq := linear_ordered_comm_ring.decidable_eq real.linear_ordered_comm_ring, decidable_lt := linear_ordered_comm_ring.decidable_lt real.linear_ordered_comm_ring, max := linear_ordered_comm_ring.max real.linear_ordered_comm_ring, max_def := _, min := linear_ordered_comm_ring.min real.linear_ordered_comm_ring, min_def := _, mul_comm := _, inv := has_inv.inv real.has_inv, div := field.div._default linear_ordered_comm_ring.mul linear_ordered_comm_ring.mul_assoc linear_ordered_comm_ring.one linear_ordered_comm_ring.one_mul linear_ordered_comm_ring.mul_one linear_ordered_comm_ring.npow linear_ordered_comm_ring.npow_zero' linear_ordered_comm_ring.npow_succ' has_inv.inv, div_eq_mul_inv := real.linear_ordered_field._proof_1, zpow := field.zpow._default linear_ordered_comm_ring.mul linear_ordered_comm_ring.mul_assoc linear_ordered_comm_ring.one linear_ordered_comm_ring.one_mul linear_ordered_comm_ring.mul_one linear_ordered_comm_ring.npow linear_ordered_comm_ring.npow_zero' linear_ordered_comm_ring.npow_succ' has_inv.inv, zpow_zero' := real.linear_ordered_field._proof_2, zpow_succ' := real.linear_ordered_field._proof_3, zpow_neg' := real.linear_ordered_field._proof_4, rat_cast := coe coe_to_lift, mul_inv_cancel := real.linear_ordered_field._proof_5, inv_zero := real.linear_ordered_field._proof_6, rat_cast_mk := real.linear_ordered_field._proof_7, qsmul := field.qsmul._default coe linear_ordered_comm_ring.add linear_ordered_comm_ring.add_assoc linear_ordered_comm_ring.zero linear_ordered_comm_ring.zero_add linear_ordered_comm_ring.add_zero linear_ordered_comm_ring.nsmul linear_ordered_comm_ring.nsmul_zero' linear_ordered_comm_ring.nsmul_succ' linear_ordered_comm_ring.neg linear_ordered_comm_ring.sub linear_ordered_comm_ring.sub_eq_add_neg linear_ordered_comm_ring.zsmul linear_ordered_comm_ring.zsmul_zero' linear_ordered_comm_ring.zsmul_succ' linear_ordered_comm_ring.zsmul_neg' linear_ordered_comm_ring.add_left_neg linear_ordered_comm_ring.add_comm linear_ordered_comm_ring.int_cast linear_ordered_comm_ring.nat_cast linear_ordered_comm_ring.one linear_ordered_comm_ring.nat_cast_zero linear_ordered_comm_ring.nat_cast_succ linear_ordered_comm_ring.int_cast_of_nat linear_ordered_comm_ring.int_cast_neg_succ_of_nat linear_ordered_comm_ring.mul linear_ordered_comm_ring.mul_assoc linear_ordered_comm_ring.one_mul linear_ordered_comm_ring.mul_one linear_ordered_comm_ring.npow linear_ordered_comm_ring.npow_zero' linear_ordered_comm_ring.npow_succ' linear_ordered_comm_ring.left_distrib linear_ordered_comm_ring.right_distrib, qsmul_eq_mul' := real.linear_ordered_field._proof_8}

source

@[protected, instance]

noncomputable def real.linear_ordered_add_comm_group :

linear_ordered_add_comm_group ℝ

Equations

real.linear_ordered_add_comm_group = linear_ordered_ring.to_linear_ordered_add_comm_group

source

@[protected, instance]

noncomputable def real.field :

field ℝ

Equations

real.field = linear_ordered_field.to_field ℝ

source

@[protected, instance]

noncomputable def real.division_ring :

division_ring ℝ

Equations

real.division_ring = field.to_division_ring ℝ

source

@[protected, instance]

noncomputable def real.decidable_lt (a b : ℝ) :

decidable (a < b)

Equations

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

source

@[protected, instance]

noncomputable def real.decidable_le (a b : ℝ) :

decidable (a ≤ b)

Equations

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

source

@[protected, instance]

noncomputable def real.decidable_eq (a b : ℝ) :

decidable (a = b)

Equations

a.decidable_eq b = classical.prop_decidable (a = b)

source

@[protected, instance]

meta def real.has_repr :

has_repr ℝ

Show an underlying cauchy sequence for real numbers.

The representative chosen is the one passed in the VM to quot.mk, so two cauchy sequences converging to the same number may be printed differently.

source

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

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

source

theorem real.mk_le_of_forall_le {f : cau_seq ℚ has_abs.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 ℚ has_abs.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

real.floor_ring = archimedean.floor_ring ℝ

source

theorem real.is_cau_seq_iff_lift {f : ℕ → ℚ} :

is_cau_seq has_abs.abs f ↔ is_cau_seq has_abs.abs (λ (i : ℕ), ↑(f i))

source

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

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

real.has_Sup = {Sup := λ (S : set ℝ), dite (S.nonempty ∧ bdd_above S) (λ (h : S.nonempty ∧ bdd_above S), classical.some _) (λ (h : ¬(S.nonempty ∧ bdd_above S)), 0)}

source

theorem real.Sup_def (S : set ℝ) :

has_Sup.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 (has_Sup.Sup S)

source

@[protected, instance]

noncomputable def real.has_Inf :

has_Inf ℝ

Equations

real.has_Inf = {Inf := λ (S : set ℝ), -has_Sup.Sup (-S)}

source

theorem real.Inf_def (S : set ℝ) :

has_Inf.Inf S = -has_Sup.Sup (-S)

source

@[protected]

theorem real.is_glb_Inf (S : set ℝ) (h₁ : S.nonempty) (h₂ : bdd_below S) :

is_glb S (has_Inf.Inf S)

source

@[protected, instance]

noncomputable def real.conditionally_complete_linear_order :

conditionally_complete_linear_order ℝ

Equations

real.conditionally_complete_linear_order = {sup := lattice.sup real.lattice, 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 := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf real.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup real.has_Sup, Inf := has_Inf.Inf real.has_Inf, le_cSup := real.conditionally_complete_linear_order._proof_1, cSup_le := real.conditionally_complete_linear_order._proof_2, cInf_le := real.conditionally_complete_linear_order._proof_3, le_cInf := real.conditionally_complete_linear_order._proof_4, le_total := _, decidable_le := linear_order.decidable_le real.linear_order, decidable_eq := linear_order.decidable_eq real.linear_order, decidable_lt := linear_order.decidable_lt real.linear_order, max_def := _, min_def := _}

source

theorem real.lt_Inf_add_pos {s : set ℝ} (h : s.nonempty) {ε : ℝ} (hε : 0 < ε) :

∃ (a : ℝ) (H : a ∈ s), a < has_Inf.Inf s + ε

source

theorem real.add_neg_lt_Sup {s : set ℝ} (h : s.nonempty) {ε : ℝ} (hε : ε < 0) :

∃ (a : ℝ) (H : a ∈ s), has_Sup.Sup s + ε < a

source

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 + ε)

source

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)

source

@[simp]

theorem real.Sup_empty :

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

has_Sup.Sup s = 0

source

theorem real.supr_of_not_bdd_above {α : Sort u_1} {f : α → ℝ} (hf : ¬bdd_above (set.range f)) :

(⨆ (i : α), f i) = 0

source

theorem real.Sup_univ :

has_Sup.Sup set.univ = 0

source

@[simp]

theorem real.Inf_empty :

has_Inf.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) :

has_Inf.Inf s = 0

source

theorem real.infi_of_not_bdd_below {α : Sort u_1} {f : α → ℝ} (hf : ¬bdd_below (set.range f)) :

(⨅ (i : α), f i) = 0

source

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

0 ≤ has_Sup.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 ≤ Sup S.

source

@[protected]

theorem real.supr_nonneg {ι : Sort u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) :

0 ≤ ⨆ (i : ι), f i

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 f i is nonnegative to show that 0 ≤ ⨆ i, f i.

source

@[protected]

theorem real.Sup_le {S : set ℝ} {a : ℝ} (hS : ∀ (x : ℝ), x ∈ S → x ≤ a) (ha : 0 ≤ a) :

has_Sup.Sup S ≤ a

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 all elements of S are bounded by a nonnagative number to show that Sup S is bounded by this number.

source

@[protected]

theorem real.supr_le {ι : Sort u_1} {f : ι → ℝ} {a : ℝ} (hS : ∀ (i : ι), f i ≤ a) (ha : 0 ≤ a) :

(⨆ (i : ι), f i) ≤ a

source

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

has_Sup.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 ≤ has_Inf.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) :

has_Inf.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) :

has_Inf.Inf s ≤ has_Sup.Sup s

source

theorem real.cau_seq_converges (f : cau_seq ℝ has_abs.abs) :

∃ (x : ℝ), f ≈ cau_seq.const has_abs.abs x

source

@[protected, instance]

def real.has_abs.abs.cau_seq.is_complete :

cau_seq.is_complete ℝ has_abs.abs

mathlib3 documentation

Real numbers from Cauchy sequences #