Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cauchy_seq_finset_of_geometric_bound

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 cauchy_seq_finset_of_geometric_boundView on Github →
2020-03-18 23:51
src/analysis/specific_limits.lean
feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171) …
Added cauchy_seq_finset_of_geometric_boundView on Github →