Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.lim_eq_of_equiv_const

Modification history

2018-11-05 17:46

data/real/basic.lean

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

Deleted real.lim_eq_of_equiv_const View on Github →

2018-08-28 10:22

data/real/basic.lean

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

Added real.lim_eq_of_equiv_const View on Github →