cau_seq): more lemmas about sup and inf (#16553)

Commit

3 years ago

feat(data/real/cau_seq): more lemmas about sup and inf (#16553) These will be needed to provide `distrib_lattice real` in terms of these operators later.

Author

eric-wieser

Committer

b-mehta

Parents

51fbf041

mathlib 5cec10d0 - feat(data/real/cau_seq): more lemmas about sup and inf (#16553)

mathlib
5cec10d0 - feat(data/real/cau_seq): more lemmas about sup and inf (#16553)