Commit 2020-10-14 14:46 de463493

View on Github →

feat(data/set/intervals): more lemmas about unordered_interval (#4607) Add images/preimages of unordered intervals under common arithmetic operations.

Estimated changes

Modified src/data/set/basic.lean

modified theorem set.nonempty.image_const

Modified src/data/set/intervals/unordered_interval.lean

added theorem set.image_add_const_interval

added theorem set.image_const_add_interval

added theorem set.image_const_mul_interval

added theorem set.image_const_sub_interval

added theorem set.image_div_const_interval

added theorem set.image_mul_const_interval

added theorem set.image_neg_interval

added theorem set.image_sub_const_interval

added theorem set.preimage_add_const_interval

added theorem set.preimage_const_add_interval

added theorem set.preimage_const_mul_interval

added theorem set.preimage_const_sub_interval

added theorem set.preimage_div_const_interval

added theorem set.preimage_mul_const_interval

added theorem set.preimage_neg_interval

added theorem set.preimage_sub_const_interval