Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 10:22 de67f542

View on Github →

feat(data/real): cauchy sequence limit lemmas (#61)

Estimated changes

Modified data/real/basic.lean

added theorem real.eq_lim_of_const_equiv

added theorem real.lim_add

added theorem real.lim_const

added theorem real.lim_eq_lim_of_equiv

added theorem real.lim_eq_of_equiv_const

added theorem real.lim_eq_zero_iff

added theorem real.lim_inv

added theorem real.lim_mul

added theorem real.lim_mul_lim

added theorem real.lim_neg

Modified data/real/cau_seq.lean

added theorem cau_seq.const_inv