Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-27 17:34 01b1576c

View on Github →

feat(topology/algebra/infinite_sum): prove cauchy_seq_of_edist_le_of_summable (#1739)

  • feat(topology/algebra/infinite_sum): prove cauchy_seq_of_edist_le_of_summable Other changes:
  • Add estimates on the distance to the limit (dist version only)
  • Simplify some proofs
  • Add some supporting lemmas
  • Fix a typo in a lemma name in ennreal
  • Add move_cast attrs
  • More *_cast tags, use norm_cast

Estimated changes

modified theorem ennreal.coe_add
modified theorem ennreal.coe_bit0
modified theorem ennreal.coe_bit1
modified theorem ennreal.coe_eq_coe
modified theorem ennreal.coe_eq_one
modified theorem ennreal.coe_eq_zero
modified theorem ennreal.coe_finset_prod
modified theorem ennreal.coe_finset_sum
modified theorem ennreal.coe_le_coe
modified theorem ennreal.coe_lt_coe
added theorem ennreal.coe_max
added theorem ennreal.coe_min
added theorem ennreal.coe_mono
modified theorem ennreal.coe_mul
modified theorem ennreal.coe_nonneg
modified theorem ennreal.coe_pos
added theorem ennreal.coe_pow
modified theorem ennreal.coe_sub
modified theorem ennreal.one_eq_coe
added theorem ennreal.one_lt_coe_iff
deleted theorem ennreal.one_lt_zero_iff
modified theorem ennreal.zero_eq_coe
added theorem nnreal.coe_pow
deleted theorem nnreal.mul_le_if_le_inv
modified theorem nnreal.prod_coe
modified theorem nnreal.smul_coe
added theorem nnreal.sub_def
added theorem nnreal.sub_pos
modified theorem nnreal.sum_coe
added theorem nnreal.dist_eq
added theorem nnreal.nndist_eq