Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm_sub_le_of_geometric_bound_of_has_sum

Modification history

2022-11-17 13:13
src/analysis/specific_limits/normed.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified norm_sub_le_of_geometric_bound_of_has_sumView on Github →
2020-03-18 23:51
src/analysis/specific_limits.lean
feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171) …
Added norm_sub_le_of_geometric_bound_of_has_sumView on Github →