Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 17:46 53d4883f

View on Github →

refactor(cau_seq): unify real.lim, complex.lim and cau_seq.lim (#433)

Estimated changes

Modified analysis/real.lean

Modified data/complex/basic.lean

deleted theorem complex.eq_lim_of_const_equiv

deleted theorem complex.equiv_lim

added theorem complex.equiv_lim_aux

deleted theorem complex.im_const_equiv_of_const_equiv

modified theorem complex.is_cau_seq_conj

modified theorem complex.lim_abs

deleted theorem complex.lim_add

modified theorem complex.lim_conj

deleted theorem complex.lim_const

added theorem complex.lim_eq_lim_im_add_lim_re

deleted theorem complex.lim_eq_lim_of_equiv

deleted theorem complex.lim_eq_of_equiv_const

deleted theorem complex.lim_eq_zero_iff

added theorem complex.lim_im

deleted theorem complex.lim_inv

deleted theorem complex.lim_mul

deleted theorem complex.lim_mul_lim

deleted theorem complex.lim_neg

added theorem complex.lim_re

deleted theorem complex.re_const_equiv_of_const_equiv

Modified data/complex/exponential.lean

Modified data/padics/hensel.lean

Modified data/padics/padic_integers.lean

Modified data/padics/padic_numbers.lean

Modified data/real/basic.lean

deleted theorem real.eq_lim_of_const_equiv

deleted theorem real.equiv_lim

deleted theorem real.le_lim

deleted theorem real.lim_add

deleted theorem real.lim_const

deleted theorem real.lim_eq_lim_of_equiv

deleted theorem real.lim_eq_of_equiv_const

deleted theorem real.lim_eq_zero_iff

deleted theorem real.lim_inv

deleted theorem real.lim_le

deleted theorem real.lim_lt

deleted theorem real.lim_mul

deleted theorem real.lim_mul_lim

deleted theorem real.lim_neg

deleted theorem real.lt_lim

Modified data/real/cau_seq.lean

modified theorem cau_seq.const_equiv

deleted theorem cau_seq.mul_lim_zero

added theorem cau_seq.mul_lim_zero_left

added theorem cau_seq.mul_lim_zero_right

Modified data/real/cau_seq_completion.lean

modified theorem cau_seq.complete

added theorem cau_seq.eq_lim_of_const_equiv

added theorem cau_seq.equiv_lim

added theorem cau_seq.le_lim

added theorem cau_seq.lim_add

added theorem cau_seq.lim_const

added theorem cau_seq.lim_eq_lim_of_equiv

added theorem cau_seq.lim_eq_of_equiv_const

added theorem cau_seq.lim_eq_zero_iff

added theorem cau_seq.lim_inv

added theorem cau_seq.lim_le

added theorem cau_seq.lim_lt

added theorem cau_seq.lim_mul

added theorem cau_seq.lim_mul_lim

added theorem cau_seq.lim_neg

deleted theorem cau_seq.lim_spec

added theorem cau_seq.lt_lim

Modified data/real/cau_seq_filter.lean