Commit 2021-03-17 12:41 1f50530a
View on Github →feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629)
This commit introduces a has_exists_add_of_le typeclass extending ordered_add_comm_monoid; is the assumption needed so that additively translating an interval gives a bijection. We then prove this fact for all flavours of interval.
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Correct.20setting.20for.20positive.20shifts.20of.20intervals