Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-15 07:59 04cac958

View on Github →

feat(data/real): reals from first principles This is beginning work on a simpler implementation of real numbers, based on Cauchy sequences, to help alleviate some of the issues we have seen with loading times and timeouts when working with real numbers. If everything goes according to plan, analysis/real.lean will be the development for the topology of the reals, but the initial construction will have no topology prerequisites.

Estimated changes

added theorem abs_pos_iff
added def vector_space.dim
added theorem bool.of_to_bool_iff
modified theorem int.cast_id
added theorem int.eq_cast
modified theorem nat.cast_id
added theorem nat.eq_cast'
added theorem nat.eq_cast
added theorem rat.eq_cast
added theorem rat.eq_cast_of_ne_zero
added theorem NEW.real.archimedean
added theorem NEW.real.inv_mk
added theorem NEW.real.inv_zero
added def NEW.real.mk
added theorem NEW.real.mk_add
added theorem NEW.real.mk_eq
added theorem NEW.real.mk_eq_mk
added theorem NEW.real.mk_eq_zero
added theorem NEW.real.mk_le
added theorem NEW.real.mk_lt
added theorem NEW.real.mk_mul
added theorem NEW.real.mk_neg
added theorem NEW.real.mk_pos
added def NEW.real.of_rat
added theorem NEW.real.of_rat_add
added theorem NEW.real.of_rat_lt
added theorem NEW.real.of_rat_mul
added theorem NEW.real.of_rat_neg
added theorem NEW.real.of_rat_one
added theorem NEW.real.of_rat_sub
added theorem NEW.real.of_rat_zero
added def NEW.real
added theorem exists_forall_ge_and
added theorem rat.cau_seq.add_apply
added theorem rat.cau_seq.add_pos
added theorem rat.cau_seq.bounded'
added theorem rat.cau_seq.bounded
added theorem rat.cau_seq.cauchy
added theorem rat.cau_seq.cauchy₂
added theorem rat.cau_seq.cauchy₃
added theorem rat.cau_seq.ext
added def rat.cau_seq.inv
added theorem rat.cau_seq.inv_apply
added theorem rat.cau_seq.inv_aux
added theorem rat.cau_seq.le_total
added theorem rat.cau_seq.lt_irrefl
added theorem rat.cau_seq.lt_trans
added theorem rat.cau_seq.mul_apply
added theorem rat.cau_seq.mul_pos
added theorem rat.cau_seq.neg_apply
added theorem rat.cau_seq.of_rat_add
added theorem rat.cau_seq.of_rat_mul
added theorem rat.cau_seq.of_rat_neg
added theorem rat.cau_seq.of_rat_pos
added theorem rat.cau_seq.of_rat_sub
added theorem rat.cau_seq.one_apply
added def rat.cau_seq.pos
added theorem rat.cau_seq.sub_apply
added theorem rat.cau_seq.trichotomy
added theorem rat.cau_seq.zero_apply
added def rat.cau_seq
deleted theorem of_to_bool_iff