intervals): more lemmas about `unordered_interval` (#4607)

Commit

5 years ago

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

References

#4925 - Make prime-avoidance branch build

Author

urkud

Parents

442ef226

mathlib de463493 - feat(data/set/intervals): more lemmas about `unordered_interval` (#4607)

mathlib
de463493 - feat(data/set/intervals): more lemmas about `unordered_interval` (#4607)