cau_seq): downgrade a proof (#17791)

Commit

3 years ago

feat(data/real/cau_seq): downgrade a proof (#17791) Switch to a lower-tech proof that a Cauchy sequence is bounded, avoiding the big-operators import.

Author

hrmacbeth

Parents

6d582e0f

mathlib e5178d62 - feat(data/real/cau_seq): downgrade a proof (#17791)

mathlib
e5178d62 - feat(data/real/cau_seq): downgrade a proof (#17791)