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 ℚ
.
- cauchy : cau_seq.completion.Cauchy
The type ℝ
of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.
Instances for real
- finite_dimensional.complex_to_real
- is_R_or_C.to_normed_algebra
- uniform_convex_space.to_strict_convex_space
- module.complex_to_real
- star_module.complex_to_real
- real.is_scalar_tower
- is_R_or_C.algebra_map_coe
- normed_space.complex_to_real
- real.has_sizeof_inst
- real.has_zero
- real.has_one
- real.has_add
- real.has_neg
- real.has_mul
- real.has_inv
- real.comm_ring
- real.has_rat_cast
- real.ring
- real.comm_semiring
- real.semiring
- real.comm_monoid_with_zero
- real.monoid_with_zero
- real.add_comm_group
- real.add_group
- real.add_comm_monoid
- real.add_monoid
- real.add_left_cancel_semigroup
- real.add_right_cancel_semigroup
- real.add_comm_semigroup
- real.add_semigroup
- real.comm_monoid
- real.monoid
- real.comm_semigroup
- real.semigroup
- real.has_sub
- real.module
- real.inhabited
- real.star_ring
- real.has_trivial_star
- real.has_lt
- real.has_le
- real.partial_order
- real.preorder
- real.ordered_comm_ring
- real.ordered_ring
- real.ordered_semiring
- real.ordered_add_comm_group
- real.ordered_cancel_add_comm_monoid
- real.ordered_add_comm_monoid
- real.nontrivial
- real.linear_order
- real.linear_ordered_comm_ring
- real.linear_ordered_ring
- real.linear_ordered_semiring
- real.is_domain
- real.linear_ordered_field
- real.linear_ordered_add_comm_group
- real.field
- real.division_ring
- real.distrib_lattice
- real.lattice
- real.semilattice_inf
- real.semilattice_sup
- real.has_inf
- real.has_sup
- real.has_repr
- real.archimedean
- real.floor_ring
- real.has_Sup
- real.has_Inf
- real.conditionally_complete_linear_order
- real.has_abs.abs.cau_seq.is_complete
- nnreal.real.has_coe
- nnreal.can_lift
- real.pseudo_metric_space
- real.order_topology
- real.metric_space
- real.noncompact_space
- real.has_continuous_star
- real.uniform_add_group
- real.topological_add_group
- real.proper_space
- real.topological_space.second_countable_topology
- real.topological_ring
- real.complete_space
- nnreal.real.has_continuous_smul
- real.star_ordered_ring
- complex.has_coe
- complex.real.can_lift
- complex.star_module
- complex.finite_dimensional
- module.real_complex_tower
- group_seminorm.fun_like
- add_group_seminorm.fun_like
- add_group_seminorm.zero_hom_class
- real.has_lipschitz_add
- real.has_bounded_smul
- real.normed_add_comm_group
- real.normed_field
- real.densely_normed_field
- real.normed_linear_ordered_field
- real.normed_lattice_add_comm_group
- real.cstar_ring
- finite_dimensional.is_R_or_C_to_real
- real.is_R_or_C
- real.angle.has_coe
- real.has_pow
- nnreal.real.has_pow
- ennreal.real.has_pow
- real.conditionally_complete_linear_ordered_field
- ereal.has_coe
- ereal.real.can_lift
- real.measurable_space
- real.borel_space
- inner_product_space.complex_to_real
- real.has_measurable_pow
- nnreal.has_measurable_pow
- ennreal.has_measurable_pow
- real.measure_space
- seminorm.zero_hom_class
- normed_space.to_locally_convex_space
- weak_bilin.locally_convex_space
- quaternion.has_inner
- quaternion.inner_product_space
- quaternion.normed_algebra
- measure_theory.jordan_decomposition.has_smul_real
- hyperreal.has_coe_t
- affine.simplex.finite_dimensional_direction_altitude
The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals.
Equations
- 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}
Equations
- real.has_zero = {zero := zero}
Equations
- real.has_inv = {inv := inv'}
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}
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 := λ (a b : ℝ), a + -b, 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 := λ (n : ℤ), ⟨↑n⟩, nat_cast := λ (n : ℕ), ⟨↑n⟩, 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}
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.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- real.inhabited = {default := 0}
The real numbers are a *
-ring, with the trivial *
-structure.
Equations
Make a real number from a Cauchy sequence of rationals (by taking the equivalence class).
Equations
- real.mk x = ⟨cau_seq.completion.mk x⟩
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}
Equations
Equations
- real.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.ordered_comm_ring._proof_1, zero_le_one := real.ordered_comm_ring._proof_2, mul_pos := real.mul_pos, mul_comm := _}
Equations
Equations
- real.linear_order = {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 := _, le_total := real.linear_order._proof_1, decidable_le := λ (a b : ℝ), classical.prop_decidable (a ≤ b), decidable_eq := decidable_eq_of_decidable_le (λ (a b : ℝ), classical.prop_decidable (a ≤ b)), decidable_lt := decidable_lt_of_decidable_le (λ (a b : ℝ), classical.prop_decidable (a ≤ b)), max := max_default (λ (a b : ℝ), classical.prop_decidable (a ≤ b)), max_def := real.linear_order._proof_2, min := min_default (λ (a b : ℝ), classical.prop_decidable (a ≤ b)), min_def := real.linear_order._proof_3}
Equations
- real.linear_ordered_comm_ring = {add := ordered_ring.add real.ordered_ring, add_assoc := _, zero := ordered_ring.zero real.ordered_ring, zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul real.ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg real.ordered_ring, sub := ordered_ring.sub real.ordered_ring, sub_eq_add_neg := _, zsmul := ordered_ring.zsmul real.ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ordered_ring.int_cast real.ordered_ring, nat_cast := ordered_ring.nat_cast real.ordered_ring, one := ordered_ring.one real.ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ordered_ring.mul real.ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ordered_ring.npow real.ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_ring.le real.ordered_ring, lt := ordered_ring.lt real.ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, 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 := _, exists_pair_ne := _, mul_comm := _}
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 := _, 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 := _, exists_pair_ne := _, 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}
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- a.decidable_lt b = has_lt.lt.decidable a b
Equations
- a.decidable_le b = has_le.le.decidable a b
Equations
- a.decidable_eq b = classical.prop_decidable (a = b)
Equations
Equations
- real.has_Inf = {Inf := λ (S : set ℝ), -has_Sup.Sup (-S)}
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 := _}
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
.
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
.
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
.
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
.