(Pre)images of intervals #
In this file we prove a bunch of trivial lemmas like “if we add
a to all points of
then we get
[a + b, a + c]”. For the functions
x ↦ x ± a,
x ↦ a ± x, and
x ↦ -x we prove
lemmas about preimages and images of all intervals. We also prove a few lemmas about images under
x ↦ a * x,
x ↦ x * a and
x ↦ x⁻¹.
The lemmas in this section state that addition maps intervals bijectively. The typeclass
has_exists_add_of_le is defined specifically to make them work when combined with
ordered_cancel_add_comm_monoid; the lemmas below therefore apply to all
ordered_add_comm_group, but also to
ℝ≥0, which are not groups.
TODO : move as much as possible in this file to the setting of this weaker typeclass.