Commit 2022-09-19 18:53 eb7d2664

View on Github →

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.

Estimated changes