Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-23 03:07 65c5cb92

View on Github →

refactor(data/real): generalize cau_seq to arbitrary metrics the intent is to use this also for the complex numbers

Estimated changes

added theorem complex.abs_div
added theorem complex.abs_inv
modified theorem complex.abs_neg
modified theorem complex.abs_pos
modified theorem complex.abs_sub
modified theorem complex.abs_sub_le
deleted theorem cau_seq.add_apply
deleted theorem cau_seq.add_lim_zero
deleted theorem cau_seq.add_pos
deleted theorem cau_seq.bounded'
deleted theorem cau_seq.bounded
deleted theorem cau_seq.cauchy
deleted theorem cau_seq.cauchy₂
deleted theorem cau_seq.cauchy₃
deleted def cau_seq.const
deleted theorem cau_seq.const_add
deleted theorem cau_seq.const_apply
deleted theorem cau_seq.const_equiv
deleted theorem cau_seq.const_inj
deleted theorem cau_seq.const_le
deleted theorem cau_seq.const_lim_zero
deleted theorem cau_seq.const_lt
deleted theorem cau_seq.const_mul
deleted theorem cau_seq.const_neg
deleted theorem cau_seq.const_pos
deleted theorem cau_seq.const_sub
deleted theorem cau_seq.equiv_def₃
deleted theorem cau_seq.exists_gt
deleted theorem cau_seq.exists_lt
deleted theorem cau_seq.ext
deleted def cau_seq.inv
deleted theorem cau_seq.inv_apply
deleted theorem cau_seq.inv_aux
deleted theorem cau_seq.inv_mul_cancel
deleted theorem cau_seq.le_antisymm
deleted theorem cau_seq.le_total
deleted def cau_seq.lim_zero
deleted theorem cau_seq.lim_zero_congr
deleted theorem cau_seq.lt_irrefl
deleted theorem cau_seq.lt_of_eq_of_lt
deleted theorem cau_seq.lt_of_lt_of_eq
deleted theorem cau_seq.lt_total
deleted theorem cau_seq.lt_trans
deleted theorem cau_seq.mul_apply
deleted theorem cau_seq.mul_lim_zero
deleted theorem cau_seq.mul_pos
deleted theorem cau_seq.neg_apply
deleted theorem cau_seq.neg_lim_zero
deleted def cau_seq.of_eq
deleted theorem cau_seq.of_near
deleted theorem cau_seq.one_apply
deleted def cau_seq.pos
deleted theorem cau_seq.pos_add_lim_zero
deleted theorem cau_seq.sub_apply
deleted theorem cau_seq.sub_lim_zero
deleted theorem cau_seq.trichotomy
deleted theorem cau_seq.zero_apply
deleted theorem cau_seq.zero_lim_zero
deleted def cau_seq
deleted theorem exists_forall_ge_and
deleted theorem is_cau_seq.cauchy₂
deleted theorem is_cau_seq.cauchy₃
deleted def is_cau_seq
deleted theorem rat_add_continuous_lemma
deleted theorem rat_inv_continuous_lemma
deleted theorem rat_mul_continuous_lemma
modified theorem real.cau_seq_converges
modified theorem real.equiv_lim
deleted def real.irrational
modified theorem real.is_cau_seq_iff_lift
modified theorem real.le_mk_of_forall_le
modified def real.mk
modified theorem real.mk_add
modified theorem real.mk_le
modified theorem real.mk_le_of_forall_le
modified theorem real.mk_lt
modified theorem real.mk_mul
modified theorem real.mk_near_of_forall_near
modified theorem real.mk_neg
modified theorem real.mk_pos
modified def real.of_rat
modified def real.sqrt_aux
modified theorem real.sqrt_aux_nonneg
deleted theorem real.sqrt_two_irrational
modified def real
added theorem cau_seq.add_apply
added theorem cau_seq.add_lim_zero
added theorem cau_seq.add_pos
added theorem cau_seq.bounded'
added theorem cau_seq.bounded
added theorem cau_seq.cauchy
added theorem cau_seq.cauchy₂
added theorem cau_seq.cauchy₃
added def cau_seq.const
added theorem cau_seq.const_add
added theorem cau_seq.const_apply
added theorem cau_seq.const_equiv
added theorem cau_seq.const_inj
added theorem cau_seq.const_le
added theorem cau_seq.const_lim_zero
added theorem cau_seq.const_lt
added theorem cau_seq.const_mul
added theorem cau_seq.const_neg
added theorem cau_seq.const_pos
added theorem cau_seq.const_sub
added theorem cau_seq.equiv_def₃
added theorem cau_seq.exists_gt
added theorem cau_seq.exists_lt
added theorem cau_seq.ext
added def cau_seq.inv
added theorem cau_seq.inv_apply
added theorem cau_seq.inv_aux
added theorem cau_seq.inv_mul_cancel
added theorem cau_seq.le_antisymm
added theorem cau_seq.le_total
added def cau_seq.lim_zero
added theorem cau_seq.lim_zero_congr
added theorem cau_seq.lt_irrefl
added theorem cau_seq.lt_of_eq_of_lt
added theorem cau_seq.lt_of_lt_of_eq
added theorem cau_seq.lt_total
added theorem cau_seq.lt_trans
added theorem cau_seq.mul_apply
added theorem cau_seq.mul_lim_zero
added theorem cau_seq.mul_pos
added theorem cau_seq.neg_apply
added theorem cau_seq.neg_lim_zero
added def cau_seq.of_eq
added theorem cau_seq.of_near
added theorem cau_seq.one_apply
added def cau_seq.pos
added theorem cau_seq.sub_apply
added theorem cau_seq.sub_lim_zero
added theorem cau_seq.trichotomy
added theorem cau_seq.zero_apply
added theorem cau_seq.zero_lim_zero
added def cau_seq
added theorem exists_forall_ge_and
added theorem is_cau_seq.cauchy₂
added theorem is_cau_seq.cauchy₃
added def is_cau_seq
added def irrational
added theorem sqrt_two_irrational