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

Parents

043a74e2

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

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