Commit 2022-09-19 07:18 7cfeb2fa

View on Github →

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.

Estimated changes