mathlib

7cfeb2fa - feat(data/real/cau_seq): define sup and inf (#16494)

feat(data/real/cau_seq): define sup and inf (#16494) Showing that these coincide with the max and min (respectively) of `real` is left to a follow-up PR. Note that these do not form a `distrib_lattice` as `cau_seq` does not form a `partial_order`.