group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060)

Commit

4 years ago

chore(analysis/normed/group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060) Add `cauchy_seq_finset_of_norm_bounded_eventually`, use it to golf some proofs.

Author

urkud

Parents

fc12ca8d

mathlib3 880182d6 - chore(analysis/normed/group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060)

mathlib3
880182d6 - chore(analysis/normed/group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060)