mathlib3
fd623d6c - feat(data/set/intervals/image_preimage): new file (#2958)

Commit
5 years ago
feat(data/set/intervals/image_preimage): new file (#2958) * Create a file for lemmas like `(λ x, x + a) '' Icc b c = Icc (b + a) (b + c)`. * Prove lemmas about images and preimages of all intervals under `x ↦ x ± a`, `x ↦ a ± x`, and `x ↦ -x`. * Move lemmas about multiplication from `basic`.
Author
Parents
Loading