Commit 2021-06-11 13:26 e35438bb
View on Github →feat(analysis): Cauchy sequence and series lemmas (#7858)
from LTE. Mostly relaxing assumptions from metric to
pseudo-metric and proving some obvious lemmas.
eventually_constant_prod and eventually_constant_sum are duplicated by hand because to_additive gets confused by the appearance of 1.
In norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G] and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.